commutative — Mathlib

English

If G is a subgroup of Perm α with index ≤ 2, then A_α ≤ G.

Русский

Если G — подгруппа Perm α и индекс ≤ 2, то A_α ⊆ G.

LaTeX

$$$$\\text{If } G \\le \\operatorname{Perm}(\\alpha) \\text{ and } \\operatorname{index}(G) \\le 2, \\text{ then } \\operatorname{alternatingGroup}(\\alpha) \\le G.$$$$

Lean4

@[to_additive]
instance commutative [Group α] [IsCyclic α] : Std.Commutative (· * · : α → α → α) where
  comm x
    y :=
    let ⟨_, hg⟩ := IsCyclic.exists_generator (α := α)
    let ⟨_, hx⟩ := hg x
    let ⟨_, hy⟩ := hg y
    hy ▸ hx ▸ zpow_mul_comm _ _ _

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