ext' — Mathlib

English

A variant of ext: two linear equivalences are equal if they agree on all basis vectors.

Русский

Вариант расширения: два линейных эквивалента равны, если они совпадают на всех базисных вектоpах.

LaTeX

$$$$ \forall i, f_1(b_i) = f_2(b_i) \Rightarrow f_1 = f_2 $$$$

Lean4

/-- Two linear equivs are equal if they are equal on basis vectors. -/
theorem ext' {f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ :=
  by
  ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, LinearEquiv.map_smulₛₗ, h]

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