equiv — Mathlib

English

Sylow p-subgroups are mutually isomorphic; for any P,Q ∈ Sylow_p(G) there is a MulEquiv between P and Q.

Русский

Силовские p-подгруппы взаимно изоморфны; для любых P,Q ∈ Sylow_p(G) существует MulEquiv между P и Q.

LaTeX

$$$\\exists \\text{MulEquiv }\\phi:\\, P \\to Q.$$$

Lean4

/-- Sylow subgroups are isomorphic -/
noncomputable def equiv [Fact p.Prime] [Finite (Sylow p G)] (P Q : Sylow p G) : P ≃* Q :=
  by
  rw [← Classical.choose_spec (exists_smul_eq G P Q)]
  exact P.equivSMul (Classical.choose (exists_smul_eq G P Q))

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