Theorem Algebra.Presentation.dimension_reindex

Modification history

2025-06-02 12:17

Mathlib/RingTheory/Extension/Presentation/Basic.lean

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

Modified Algebra.Presentation.dimension_reindex View on Github →

2025-04-03 10:34

Mathlib/RingTheory/Presentation.lean

refactor(RingTheory/Smooth): remove universe parameters for generators and relations in `Algebra.IsStandardSmooth` (#23553) …

Added Algebra.Presentation.dimension_reindex View on Github →