Def Algebra.SubmersivePresentation.ofAlgEquiv

Modification history

2026-02-24 10:38

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

chore: bump toolchain to v4.29.0-rc2 (#35708)

Deleted Algebra.SubmersivePresentation.ofAlgEquiv View on Github →

2025-12-21 17:00

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

feat(RingTheory/Smooth/StandardSmooth): transport `IsStandardSmooth` along algebra isomorphisms (#32925)

Added Algebra.SubmersivePresentation.ofAlgEquiv View on Github →