std_basis

Stream: general

[Sebastien Gouezel]

In the linear algebra library, there is something called is_basis, and something called std_basis. But if I understand correctlystd_basis is not a basis, it is the canonical embedding of a factor into a product of modules, defined as follows.

/-- The standard basis of the product of `φ`. -/
def std_basis (i : ι) : φ i →ₗ[R] (Πi, φ i) := pi (diag i)

Should we change its name (and its docstring)?

[Sebastien Gouezel]

Also, adding docstrings to lemmas such as

lemma is_basis_fun₀ : is_basis R
    (λ (ji : Σ (j : η), (λ _, unit) j),
       (std_basis R (λ (i : η), R) (ji.fst)) 1)

could help lower the entry barrier in this part of the library :)