def MagmaA2 : Magma (Fin 3 × Fin 3)

We define Knuth's A2 here in terms of A21.

Equations

• One or more equations did not get rendered due to their size.

def MagmaA2T : Magma (Fin 9)

A magma isomorphic to A2, given as an optable.

Equations

• MagmaA2T = { op := MemoFinOp.opOfTable 196323798789606163852677465202712072601854610383330849839818960036944772449604 }

def equiv_F3xF3_F9 : Fin 3 × Fin 3 ≃ Fin 9

Fin 3 × Fin 3 is isomorphic to Fin 9 as a set.

Equations

• One or more equations did not get rendered due to their size.

def instMagmaProdFinOfNatNat : Magma (Fin 3 × Fin 3)

Equations

• instMagmaProdFinOfNatNat = MagmaA2

def instMagmaFinOfNatNat : Magma (Fin 9)

Equations

• instMagmaFinOfNatNat = MagmaA2T

def equiv_MagmaA2_MagmaA2T : Fin 3 × Fin 3 ≃◇ Fin 9

Equations

• equiv_MagmaA2_MagmaA2T = { toEquiv := equiv_F3xF3_F9, map_op' := equiv_MagmaA2_MagmaA2T.proof_1 }

theorem MagmaA2T.Facts : ∃ (G : Type) (x : Magma G), Equation168 G ∧ Equation1480 G ∧ Equation1483 G ∧ Equation1484 G ∧ Equation1485 G ∧ Equation1486 G ∧ Equation1487 G ∧ Equation2052 G ∧ Equation2089 G ∧ Equation2126 G ∧ Equation2162 G ∧ Equation2163 G ∧ Equation2164 G ∧ ¬Equation3461 G ∧ ¬Equation3462 G ∧ ¬Equation3463 G ∧ ¬Equation3521 G ∧ ¬Equation3522 G ∧ ¬Equation3523 G ∧ ¬Equation3532 G ∧ ¬Equation3533 G ∧ ¬Equation3534 G ∧ ¬Equation3535 G ∧ ¬Equation3864 G ∧ ¬Equation3880 G ∧ ¬Equation3883 G ∧ ¬Equation3915 G ∧ ¬Equation3921 G ∧ ¬Equation3952 G ∧ ¬Equation3958 G ∧ ¬Equation3989 G ∧ ¬Equation3997 G ∧ ¬Equation4001 G ∧ ¬Equation4268 G ∧ ¬Equation4282 G ∧ ¬Equation4314 G ∧ ¬Equation4315 G ∧ ¬Equation4339 G ∧ ¬Equation4357 G ∧ ¬Equation4587 G ∧ ¬Equation4606 G ∧ ¬Equation4615 G ∧ ¬Equation4645 G ∧ ¬Equation4666 G ∧ ¬Equation4689 G