right_quotientAction' — Mathlib

English

If H is normal in G, then the opposite of the normalizer acts on H by conjugation via a natural right quotient action.

Русский

Если H нормально в G, то противоположный нормализатор действует на H конъюгацией через естественное правое квотиентное действие.

LaTeX

$$$H \\trianglelefteq G \\Rightarrow (N_G(H))^{op} \\curvearrowright H,$ where $(gH) \\cdot h = g h g^{-1}$$$

Lean4

@[to_additive]
instance right_quotientAction' [hH : H.Normal] : QuotientAction αᵐᵒᵖ H :=
  ⟨fun _ _ _ _ => by
    rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc, mul_inv_cancel_right]⟩

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