eqOn_span' — Mathlib

English

If f: V → K is a linear map with f(x) ≠ 0 for some x, then span{x} ⊔ ker f = ⊤ in a finite-dimensional setting.

Русский

Если существует x такое, что f(x) ≠ 0, то спан{ x } ⊔ ker f = ⊤.

LaTeX

$$$\langle \operatorname{span} K\{x\}, \ker f \rangle = \top$$$

Lean4

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

This version uses `Set.EqOn`, and the hidden argument will expand to `h : x ∈ (span R s : Set M)`.
See `LinearMap.eqOn_span` for a version that takes `h : x ∈ span R s` as an argument. -/
theorem eqOn_span' {s : Set M} {f g : F} (H : Set.EqOn f g s) : Set.EqOn f g (span R s : Set M) :=
  eqOn_span_iff.2 H

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