Commit 2023-04-28 21:59 a87b0995

View on Github →

feat: port LinearAlgebra.Matrix.Diagonal (#3695) Some proofs in the last section were failing even with eta-experiment, so I generalized some lemmas from Fields to Semifields.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/LinearAlgebra/Basic.lean

modified theorem LinearMap.ker_smul'

Created Mathlib/LinearAlgebra/Matrix/Diagonal.lean

added theorem Matrix.diagonal_comp_stdBasis

added theorem Matrix.diagonal_toLin'

added theorem Matrix.ker_diagonal_toLin'

added theorem Matrix.proj_diagonal

added theorem Matrix.range_diagonal

added theorem Matrix.rank_diagonal