Commit 2023-08-22 10:56 7f1bdad7

View on Github →

feat: lemmas about Smith normal form and trace of restriction (#6666)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

added theorem Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord

added theorem Basis.SmithNormalForm.le_ker_coord_of_nmem_range

added theorem Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul

added theorem Basis.SmithNormalForm.repr_comp_embedding_eq_smul

added theorem Basis.SmithNormalForm.repr_eq_zero_of_nmem_range

added theorem Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix

Created Mathlib/LinearAlgebra/PID.lean

added theorem LinearMap.trace_restrict_eq_of_forall_mem