uniq — Mathlib

English

Postcomposition with the canonical solution is injective; if solution.postcomp f = solution.postcomp f', then f = f'.

Русский

Посткомпоновка с каноническим решением инъективна: если solution.postcomp f = solution.postcomp f', то f = f'.

LaTeX

$$$$ \\text{If } solution.\\mathrm{postcomp} f = solution.\\mathrm{postcomp} f' \\text{ then } f = f' $$$$

Lean4

/-- Uniqueness (up to a unique linear equivalence) of the module defined
by generators and relations. -/
noncomputable def uniq : M ≃ₗ[A] N :=
  LinearEquiv.ofLinear (h.desc solution') (h'.desc solution) (h'.postcomp_injective (by simp))
    (h.postcomp_injective (by simp))

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