commutative_iff — Mathlib

English

D_n is abelian if and only if n equals 1 or 2.

Русский

Диэдральная группа D_n абелева тогда и только тогда, когда n = 1 или n = 2.

LaTeX

$$IsAbelian(DihedralGroup(n)) \iff n = 1 \lor n = 2$$

Lean4

theorem commutative_iff : Std.Commutative (fun x y : DihedralGroup n ↦ x * y) ↔ n = 1 ∨ n = 2
    where
  mp := by contrapose!; rintro ⟨h1, h2⟩; exact not_commutative h1 h2
  mpr := by rintro (rfl | rfl) <;> exact ⟨by decide⟩

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