mulEquivCongr_apply_smul — Mathlib

English

The conjugation action of G on L corresponds to the action of the corresponding element in H under the isomorphism mulEquivCongr.

Русский

Действие G на L по совместному изоморфлению mulEquivCongr совпадает с соответствующим действием через гомоморфизм.

LaTeX

$$mulEquivCongr_apply_smul G H K L g x = g x$$

Lean4

@[simp]
theorem mulEquivCongr_apply_smul [IsGaloisGroup G K L] [Finite G] [IsGaloisGroup H K L] [Finite H] (g : G) (x : L) :
    mulEquivCongr G H K L g • x = g • x :=
  AlgEquiv.ext_iff.mp ((mulEquivAlgEquiv H K L).apply_symm_apply (mulEquivAlgEquiv G K L g)) x

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