step7 — Mathlib

English

A structural step in Schur–Zassenhaus construction showing commutativity of certain operations under induction hypotheses.

Русский

Этап индуктивного построения Шур-Цассенауска, демонстрирующий совместимость операций.

LaTeX

$$IsMulCommutative N$$

Lean4

/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
theorem step7 : IsMulCommutative N :=
  by
  haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
  haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
  exact
    ⟨⟨fun g h =>
        ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm
            g).symm⟩⟩

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