mathlib3

0b806ba6 - docs(linear_algebra): refer to `pi.basis_fun` in `pi.basis` (#14505)

docs(linear_algebra): refer to `pi.basis_fun` in `pi.basis` (#14505) This is a common question so the more ways we can point to the standard basis, the better! See also Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Standard.20basis