linearMap_qext — Mathlib

English

If two linear maps f,g from M/P to M2 agree after precomposition with the quotient map mkQ, then f = g.

Русский

Если линейные отображения f,g: M/P → M2 совпадают после предварительного композиирования с mkQ, то f = g.

LaTeX

$$$f \circ p.mkQ = g \circ p.mkQ \Rightarrow f = g$$$

Lean4

/-- Two `LinearMap`s from a quotient module are equal if their compositions with
`submodule.mkQ` are equal.

See note [partially-applied ext lemmas]. -/
@[ext high] -- Increase priority so this applies before `LinearMap.ext`

theorem linearMap_qext ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=
  LinearMap.ext fun x => Submodule.Quotient.induction_on _ x <| (LinearMap.congr_fun h :)

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