right_quotientAction — Mathlib

English

For a subgroup H of G, there is a natural right action of the opposite normalizer on the set of right cosets, reflecting the conjugation-normalizer structure.

Русский

Для подгруппы H ⊆ G существует естественное правое действие противоположного нормализатора на множество правых косет, отражающее структуру нормализации через сопряжение.

LaTeX

$$$\\text{(N_G(H))^{op} \\curvearrowright H\\backslash G}:\\; (nH) \\cdot (Hg) = Hgn^{-1}$ (правое косетное действие через нормализатор)$$

Lean4

@[to_additive]
instance right_quotientAction : QuotientAction (normalizer H).op H :=
  ⟨fun b c _ _ => by
    rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]⟩

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