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 }