Commit 2023-04-06 14:47 bd8664d7

View on Github →

feat: port LinearAlgebra.StdBasis (#3264)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/StdBasis.lean

added theorem LinearMap.coe_stdBasis

added theorem LinearMap.disjoint_stdBasis_stdBasis

added theorem LinearMap.infᵢ_ker_proj_le_supᵢ_range_stdBasis

added theorem LinearMap.ker_stdBasis

added theorem LinearMap.proj_comp_stdBasis

added theorem LinearMap.proj_stdBasis_ne

added theorem LinearMap.proj_stdBasis_same

added def LinearMap.stdBasis

added theorem LinearMap.stdBasis_apply'

added theorem LinearMap.stdBasis_apply

added theorem LinearMap.stdBasis_eq_pi_diag

added theorem LinearMap.stdBasis_eq_single

added theorem LinearMap.stdBasis_ne

added theorem LinearMap.stdBasis_same

added theorem LinearMap.supᵢ_range_stdBasis

added theorem LinearMap.supᵢ_range_stdBasis_eq_infᵢ_ker_proj

added theorem LinearMap.supᵢ_range_stdBasis_le_infᵢ_ker_proj

added theorem Matrix.stdBasis_eq_stdBasisMatrix

added theorem Pi.basisFun_apply

added theorem Pi.basisFun_repr

added theorem Pi.basis_apply

added theorem Pi.basis_repr

added theorem Pi.basis_repr_stdBasis

added theorem Pi.linearIndependent_stdBasis