Commit 2024-08-11 10:40 7bb6e8b2

View on Github →

refactor: deprecate stdBasis (#15660) Deprecate stdBasis in favor of its duplicate LinearMap.single. Also changes the binder types in the later. Note the simp normal form of an applied (or even simply coerced to function) LinearMap.single is a Pi.single, as discussed during the community meeting. See the Zulip discussion.

Estimated changes

modified theorem AffineMap.pi_ext_nonempty'
added theorem Matrix.toBilin'_single
modified theorem LinearMap.coe_single
added theorem LinearMap.ker_single
modified theorem LinearMap.pi_ext'
added theorem LinearMap.single_apply
modified theorem Pi.basisFun_apply
added theorem Pi.basis_repr_single