Commit 2025-09-13 02:46 db73ea1c

View on Github →

chore(RingTheory/Smooth): split StandardSmooth (#28725) We factor out the SubmersivePresentation part into a separate file to prepare for new content. Also the module docstrings and TODOs are updated.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Extension/Presentation/Submersive.lean

added theorem Algebra.PreSubmersivePresentation.aevalDifferential_single

added theorem Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix

added theorem Algebra.PreSubmersivePresentation.baseChange_jacobian

added theorem Algebra.PreSubmersivePresentation.baseChange_ring

added theorem Algebra.PreSubmersivePresentation.baseChange_toPresentation

added theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite

added theorem Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian

added theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_apply

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_naive

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_reindex

added theorem Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det

added theorem Algebra.PreSubmersivePresentation.jacobian_reindex

added theorem Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix

added theorem Algebra.PreSubmersivePresentation.localizationAway_jacobian

added def Algebra.PreSubmersivePresentation.naive

added theorem Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap_jacobian

added theorem Algebra.PreSubmersivePresentation.toGenerators_comp

added theorem Algebra.PreSubmersivePresentation.toPresentation_comp

added structure Algebra.PreSubmersivePresentation

added theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

added theorem Algebra.SubmersivePresentation.basisDeriv_apply

added theorem Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation

added structure Algebra.SubmersivePresentation

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

deleted theorem Algebra.PreSubmersivePresentation.aevalDifferential_single

deleted theorem Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix

deleted theorem Algebra.PreSubmersivePresentation.baseChange_jacobian

deleted theorem Algebra.PreSubmersivePresentation.baseChange_ring

deleted theorem Algebra.PreSubmersivePresentation.baseChange_toPresentation

deleted theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite

deleted theorem Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian

deleted theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

deleted theorem Algebra.PreSubmersivePresentation.jacobiMatrix_apply

deleted theorem Algebra.PreSubmersivePresentation.jacobiMatrix_naive

deleted theorem Algebra.PreSubmersivePresentation.jacobiMatrix_reindex

deleted theorem Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det

deleted theorem Algebra.PreSubmersivePresentation.jacobian_reindex

deleted theorem Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix

deleted theorem Algebra.PreSubmersivePresentation.localizationAway_jacobian

deleted def Algebra.PreSubmersivePresentation.naive

deleted theorem Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap_jacobian

deleted theorem Algebra.PreSubmersivePresentation.toGenerators_comp

deleted theorem Algebra.PreSubmersivePresentation.toPresentation_comp

deleted structure Algebra.PreSubmersivePresentation

deleted theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

deleted theorem Algebra.SubmersivePresentation.basisDeriv_apply

deleted theorem Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation

deleted structure Algebra.SubmersivePresentation