Commit 2025-01-09 15:53 1da931e9

View on Github →

feat(RingTheory/StandardSmooth): pre-requisites for calculating the naive cotangent complex of a submersive presentation (#19749) Preparations for #19748

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem Finset.prod_sum_eq_prod_toLeft_mul_prod_toRight

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.mulVec_injective_of_isUnit

added theorem Matrix.vecMul_injective_of_isUnit

Created Mathlib/LinearAlgebra/Basis/Exact.lean

added theorem LinearIndependent.linearIndependent_of_exact_of_retraction

added theorem Submodule.top_le_span_of_exact_of_retraction

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem Module.subsingleton_of_rank_zero

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Matrix.linearIndependent_cols_of_isUnit

added theorem Matrix.linearIndependent_rows_of_isUnit

Modified Mathlib/RingTheory/Extension.lean

added theorem Algebra.Extension.Cotangent.mk_eq_zero_iff

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.relation_mem_ker

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.PreSubmersivePresentation.aevalDifferential_single

added theorem Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix

added theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

added theorem Algebra.SubmersivePresentation.basisDeriv_apply

added theorem Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation