conjNormal_val — Mathlib

English

The action conjNormal on elements of H coincides with the standard ConjAct action on H.

Русский

Действие conjNormal на элементах H совпадает с обычным действием сопряжения ConjAct на H.

LaTeX

$$$ \operatorname{MulAut}.conjNormal \;h = \operatorname{MulAut}.conj\;h. $$$

Lean4

theorem _root_.MulAut.conjNormal_val {H : Subgroup G} [H.Normal] {h : H} : MulAut.conjNormal ↑h = MulAut.conj h :=
  MulEquiv.ext fun _ => rfl

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