basisSingleton — Mathlib

English

In a space of dimension 1, any nonzero vector generates a basis indexed by a unique index.

Русский

В пространстве размерности 1 любой ненулевой вектор порождает базис, индексируемый уникальным индексом.

LaTeX

$$$ basisSingleton\ ι \ h \ v \ hv : Basis ι K V $$$

Lean4

/-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/
@[simps repr_apply]
noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) : Basis ι K V :=
  let b := Module.basisUnique ι h
  have h : b.repr v default ≠ 0 := mt Module.basisUnique_repr_eq_zero_iff.mp hv
  Basis.ofRepr
    { toFun := fun w => Finsupp.single default (b.repr w default / b.repr v default)
      invFun := fun f => f default • v
      map_add' := by simp [add_div]
      map_smul' := by simp [mul_div]
      left_inv := fun w => by
        apply_fun b.repr using b.repr.toEquiv.injective
        apply_fun Equiv.finsuppUnique
        simp only [LinearEquiv.map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same, smul_eq_mul, Pi.smul_apply,
          Equiv.finsuppUnique_apply]
        exact div_mul_cancel₀ _ h
      right_inv := fun f => by
        ext
        simp only [LinearEquiv.map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same, RingHom.id_apply, smul_eq_mul,
          Pi.smul_apply]
        exact mul_div_cancel_right₀ _ h }

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