Def Algebra.Presentation.ofAlgEquiv

Modification history

2026-02-24 10:38
Mathlib/RingTheory/Extension/Presentation/Basic.lean
chore: bump toolchain to v4.29.0-rc2 (#35708)
Deleted Algebra.Presentation.ofAlgEquivView on Github →
2025-12-21 17:00
Mathlib/RingTheory/Extension/Presentation/Basic.lean
feat(RingTheory/Smooth/StandardSmooth): transport `IsStandardSmooth` along algebra isomorphisms (#32925)
Added Algebra.Presentation.ofAlgEquivView on Github →