instIsAddKleinFourProdZModOfNatNat

English

The additive Klein four instance on ZMod 2 × ZMod 2 holds: the product is Klein four with exponent 2.

Русский

На ZMod 2 × ZMod 2 выполняется структура Klein Four в аддитивной реализации:exponent 2 и четыре элемента.

LaTeX

$$IsKleinFour( (\mathbb{Z}/2\mathbb{Z}) \times (\mathbb{Z}/2\mathbb{Z}) )$$

Lean4

instance : IsAddKleinFour (ZMod 2 × ZMod 2) where
  card_four := by simp
  exponent_two := by simp [AddMonoid.exponent_prod]

Похожие утверждения