ext_on — Mathlib

English

Given a nonzero x ∈ M, there is a canonical linear equivalence between R and the span of x.

Русский

Для не нулевого x существует каноническое линейное отношение между R и спаном x.

LaTeX

$$toSpanNonzeroSingleton : R ≃ₗ[R] R ∙ x$$

Lean4

/-- If `s` generates the whole module and linear maps `f`, `g` are equal on `s`, then they are
equal. -/
theorem ext_on {s : Set M} {f g : F} (hv : span R s = ⊤) (h : Set.EqOn f g s) : f = g :=
  DFunLike.ext _ _ fun _ => eqOn_span h (eq_top_iff'.1 hv _)

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