lieModuleHom_ext — Mathlib

English

Compatibility of kernel equality with mk and mk'.

Русский

Согласованность равенства ядра с mk и mk'.

LaTeX

$$mk'_ker$$

Lean4

/-- Two `LieModuleHom`s from a quotient lie module are equal if their compositions with
`LieSubmodule.Quotient.mk'` are equal.

See note [partially-applied ext lemmas]. -/
@[ext]
theorem lieModuleHom_ext ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
  LieModuleHom.ext fun x => Quotient.inductionOn' x <| LieModuleHom.congr_fun h

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