mulEquivCongr — Mathlib

English

If G and H are finite Galois groups for L/K, then G ≅* H.

Русский

Если G и H являются конечными Галуа-группами для L/K, то G эквивалентно H.

LaTeX

$$IsGaloisGroup G K L \\land Finite G \\land IsGaloisGroup H K L \\land Finite H \\Rightarrow G \\cong_* H$$

Lean4

/-- If `G` and `H` are finite Galois groups for `L/K`, then `G` is isomorphic to `H`. -/
noncomputable def mulEquivCongr [IsGaloisGroup G K L] [Finite G] [IsGaloisGroup H K L] [Finite H] : G ≃* H :=
  (mulEquivAlgEquiv G K L).trans (mulEquivAlgEquiv H K L).symm

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