Commit 2025-06-02 12:17 966daba4

View on Github →

refactor(RingTheory): unbundle rels and vars from Algebra.Presentation (#25085)

Estimated changes

Modified Mathlib/Algebra/Module/Presentation/Differentials.lean

modified theorem Algebra.Presentation.differentials.comm₁₂_single

modified theorem Algebra.Presentation.differentials.hom₁_single

Modified Mathlib/RingTheory/Etale/Kaehler.lean

Modified Mathlib/RingTheory/Extension/Cotangent/Basic.lean

modified def Algebra.Generators.H1Cotangent.equiv

modified def Algebra.Generators.cotangentSpaceBasis

Modified Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean

modified theorem Algebra.Generators.comp_localizationAway_ker

Modified Mathlib/RingTheory/Extension/Generators.lean

modified def Algebra.Generators.baseChange

modified def Algebra.Generators.comp

modified def Algebra.Generators.extendScalars

modified def Algebra.Generators.kerCompPreimage

modified theorem Algebra.Generators.ker_comp_eq_sup

modified def Algebra.Generators.localizationAway

modified theorem Algebra.Generators.map_ofComp_ker

modified theorem Algebra.Generators.map_toComp_ker

modified def Algebra.Generators.ofAlgHom

modified def Algebra.Generators.ofComp

modified theorem Algebra.Generators.ofComp_kerCompPreimage

modified theorem Algebra.Generators.ofComp_toAlgHom_monomial_sumElim

modified def Algebra.Generators.ofSet

modified def Algebra.Generators.ofSurjective

modified theorem Algebra.Generators.reindex_val

modified def Algebra.Generators.self

modified theorem Algebra.Generators.toAlgHom_ofComp_rename

modified theorem Algebra.Generators.toAlgHom_ofComp_surjective

modified def Algebra.Generators.toComp

modified theorem Algebra.Generators.toComp_toAlgHom

modified theorem Algebra.Generators.toComp_toAlgHom_monomial

modified def Algebra.Generators.toExtendScalars

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

modified def Algebra.Presentation.baseChange

modified theorem Algebra.Presentation.comp_aeval_relation_inl

modified theorem Algebra.Presentation.comp_relation_inr

modified theorem Algebra.Presentation.dimension_reindex

added theorem Algebra.Presentation.exists_presentation_fin

added theorem Algebra.Presentation.fg_ker

modified theorem Algebra.Presentation.finitePresentation_of_isFinite

deleted theorem Algebra.Presentation.ideal_fg_of_isFinite

deleted theorem Algebra.Presentation.isFinite_reindex_iff

modified def Algebra.Presentation.ofFinitePresentation

added def Algebra.Presentation.ofFinitePresentationRels

added def Algebra.Presentation.ofFinitePresentationVars

modified theorem Algebra.Presentation.relation_mem_ker

modified structure Algebra.Presentation

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

modified def Algebra.Generators.CotangentSpace.compEquiv

modified theorem Algebra.Generators.H1Cotangent.δAux_toAlgHom

modified theorem Algebra.Generators.H1Cotangent.δ_eq_δ

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

modified theorem Algebra.PreSubmersivePresentation.aevalDifferential_single

modified theorem Algebra.PreSubmersivePresentation.baseChange_jacobian

modified theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite

modified theorem Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian

modified theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

modified theorem Algebra.PreSubmersivePresentation.jacobiMatrix_apply

modified theorem Algebra.PreSubmersivePresentation.jacobiMatrix_reindex

modified theorem Algebra.PreSubmersivePresentation.jacobian_reindex

modified structure Algebra.PreSubmersivePresentation

modified theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

modified theorem Algebra.SubmersivePresentation.basisDeriv_apply

modified theorem Algebra.SubmersivePresentation.isStandardSmooth

modified theorem Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension

modified structure Algebra.SubmersivePresentation

Modified Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

modified theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_apply

modified theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff

modified theorem Algebra.SubmersivePresentation.basisCotangent_apply

modified theorem Algebra.SubmersivePresentation.cotangentComplexAux_injective

modified theorem Algebra.SubmersivePresentation.cotangentComplexAux_surjective

modified theorem Algebra.SubmersivePresentation.free_kaehlerDifferential

modified theorem Algebra.SubmersivePresentation.rank_kaehlerDifferential

modified theorem Algebra.SubmersivePresentation.sectionCotangent_eq_iff

modified theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range