quotientToEndHom_mk — Mathlib

English

Given x ∈ H and g ∈ G, the endomorphism on G/N corresponding to x acts by left multiplication by g x^{-1} modulo N.

Русский

Пусть x ∈ H, g ∈ G. Тогда соответствующий элементу x конец в G/N действует с левой множителем g x^{-1} по модулю N.

LaTeX

$$$(\text{quotientToEndHom } H N) \ ⟦x⟧).hom ⟦g⟧ = ⟦g x^{-1}⟧$$$

Lean4

@[simp]
theorem quotientToEndHom_mk [N.Normal] (x : H) (g : G) : (quotientToEndHom H N ⟦x⟧).hom ⟦g⟧ = ⟦g * x⁻¹⟧ :=
  rfl

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