basis..sum_extend_extends

Stream: Is there code for X?

[Adam Topaz]

Do we really not have this lemma?

import linear_algebra.basis

variables {ι K M : Type*} [field K] [add_comm_group M] [module K M]

example (f : ι → M) (hf : linear_independent K f) (i : ι) :
  (basis.sum_extend hf) (sum.inl i) = f i :=
begin
  dsimp [basis.sum_extend],
  simp,
end

[Anne Baanen]

Probably not, IIRC most of these basis.extend-form lemmas were defined for their type rather than their evaulation properties.