exponent_kleinFour_of_card_eq_four

English

The exponent of Klein four is 2.

Русский

Показатель Klein–четверки равен 2.

LaTeX

$$$\operatorname{Monoid.exponent}(\mathrm{kleinFour}(\alpha)) = 2$$$

Lean4

theorem exponent_kleinFour_of_card_eq_four (hα4 : Nat.card α = 4) : Monoid.exponent (kleinFour α) = 2 :=
  by
  have : Monoid.exponent (kleinFour α) ∣ 2 := by
    rw [Monoid.exponent_dvd]
    rintro ⟨⟨g, hg⟩, hg'⟩
    simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'
    rcases hg' with hg' | hg'
    · convert one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'
    · convert pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp
  rw [Nat.dvd_prime Nat.prime_two] at this
  apply Or.resolve_left this
  rw [Monoid.exp_eq_one_iff, ← Finite.card_le_one_iff_subsingleton, kleinFour_card_of_card_eq_four hα4]
  decide

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