Using a basis of size one

Stream: maths

[Patrick Lutz]

Embarrassingly, I cannot figure out how to do the following using Lean's linear algebra library

import linear_algebra.basis

example (K V : Type*) [field K] [add_comm_group V] [vector_space K V]
    (x : V) (hx : is_basis K (coe : ({x} : set V) → V)) (y : V) :
    y = (is_basis.repr hx y ⟨x, set.mem_singleton x⟩) • x := sorry

I believe this is basically saying that if $\{x\}$ is a basis for $V$ and $y$ is in $V$ then $y$ is equal to $x$ times the coefficient of $x$ in the representation of $y$ in terms of the basis $\{x\}$. How is this sort of thing supposed to be proved?

[Floris van Doorn]

Assuming I can slightly change the problem (into - what I think is - a more convenient way of stating the example), then here is a way to do this:

import linear_algebra.basis

example (K V : Type*) [field K] [add_comm_group V] [vector_space K V]
  (x : V) (hx : is_basis K (λ _ : unit, x)) (y : V) :
  hx.repr y () • x = y :=
begin
  convert hx.total_repr y, rw [finsupp.total_apply, finsupp.sum_fintype],
  { simp only [fintype.univ_punit, finset.sum_singleton] },
  { simp only [forall_const, zero_smul] }
end

I'm not fluent in the linear algebra library, so there might be an easier way.

[Floris van Doorn]

I found both arguments to simp only by using squeeze_simp.
For the first line I had to search a little bit, but I could use the first lemma under the relevant definition (incidentally the first lemma made progress in each of the cases).

[Kenny Lau]

import linear_algebra.basis

open finsupp

theorem repr_smul_of_unique {R M ι : Type*} [ring R] [add_comm_group M] [module R M]
  [unique ι] (f : ι → M) (hx : is_basis R f) (y : M) :
  hx.repr y (default ι) • f (default ι) = y :=
by conv_rhs { rw [← hx.total_repr y, total_apply, unique_single (hx.repr y), sum_single_index],
  skip, rw zero_smul }

theorem repr_smul_of_singleton {R M : Type*} [ring R] [add_comm_group M] [module R M]
  (x : M) (hx : is_basis R (coe : ({x} : set M) → M)) (y : M) :
  hx.repr y ⟨x, set.mem_singleton x⟩ • x = y :=
repr_smul_of_unique _ hx y