Commit 2025-03-31 13:41 4d364ab4

View on Github →

feat(RingTheory/Presentation): reindex presentations (#21260) Constructs induced presentations from equivalent indexing types for generators and relations. This will be used in a follow-up to fix the universes of the generators and relations in Algebra.IsStandardSmooth to 0.

Estimated changes

Modified Mathlib/RingTheory/Generators.lean

added theorem Algebra.Generators.reindex_val

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.comap_idₐ

added theorem Ideal.map_idₐ

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.isFinite_reindex_iff

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_reindex

added theorem Algebra.PreSubmersivePresentation.jacobian_reindex