toEndHom_trivial_of_mem — Mathlib

English

If n ∈ N, then the corresponding endomorphism is the identity.

Русский

Если n ∈ N, соответствующий эндоморфизм является тождественным отображением.

LaTeX

$$$toEndHom N n = id$$$

Lean4

theorem toEndHom_trivial_of_mem [N.Normal] {n : G} (hn : n ∈ N) : toEndHom N n = 𝟙 (G ⧸ₐ N) :=
  by
  apply Action.hom_ext
  ext (x : G ⧸ N)
  induction x using Quotient.inductionOn
  exact Quotient.sound ((QuotientGroup.leftRel_apply).mpr <| by simpa)

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