not_commutative — Mathlib

English

For any n with n ≠ 1 and n ≠ 2, the dihedral group D_n is not commutative.

Русский

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

LaTeX

$$n ≠ 1 ⇒ n ≠ 2 ⇒ \text{DihedralGroup}(n) \text{ не коммутативна}$$

Lean4

theorem not_commutative : ∀ {n : ℕ}, n ≠ 1 → n ≠ 2 → ¬Std.Commutative fun (x y : DihedralGroup n) => x * y
  | 0, _, _ => fun ⟨h'⟩ ↦ by simpa using h' (r 1) (sr 0)
  | n + 3, _, _ => by
    rintro ⟨h'⟩
    specialize h' (r 1) (sr 0)
    rw [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq, neg_eq_iff_add_eq_zero, one_add_one_eq_two, ←
      ZMod.val_eq_zero, ZMod.val_two_eq_two_mod] at h'
    simpa using Nat.le_of_dvd Nat.zero_lt_two <| Nat.dvd_of_mod_eq_zero h'

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