eq_one_of_smul_eq_one — Mathlib

English

Rank(H) ≤ Index(H) · Rank(G).

Русский

Ранг H не превосходит индекс H, умноженный на ранг G.

LaTeX

$$Group.rank H ≤ H.index * Group.rank G$$

Lean4

theorem eq_one_of_smul_eq_one (hH : Nat.Coprime (Nat.card H) H.index) (α : H.QuotientDiff) (h : H) :
    h • α = α → h = 1 :=
  Quotient.inductionOn' α fun α hα =>
    (powCoprime hH).injective <|
      calc
        h ^ H.index = diff (MonoidHom.id H) (op ((h⁻¹ : H) : G) • α) α := by
          rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
        _ = 1 ^ H.index := (Quotient.exact' hα).trans (one_pow H.index).symm

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