linearMap_ext — Mathlib

English

If two linear maps from relations.Quotient agree on all generators given by toQuotient (Finsupp.single g 1), they are equal.

Русский

Если два линейных отображения из relations.Quotient совпадают на всех генераторах, заданных toQuotient (Finsupp.single g 1), они равны.

LaTeX

$$$\\forall g,\\ f( relations.toQuotient(\\mathrm{Finsupp.single} g\\ 1)) = f'( relations.toQuotient(\\mathrm{Finsupp.single} g\\ 1)) \\Rightarrow f = f'.$$$

Lean4

@[ext]
theorem linearMap_ext {M : Type v} [AddCommGroup M] [Module A M] {f f' : relations.Quotient →ₗ[A] M}
    (h :
      ∀ (g : relations.G),
        f (relations.toQuotient (Finsupp.single g 1)) = f' (relations.toQuotient (Finsupp.single g 1))) :
    f = f' :=
  Submodule.linearMap_qext _ (Finsupp.lhom_ext' (fun g ↦ LinearMap.ext_ring (h g)))

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