Theorem Algebra.PreSubmersivePresentation.jacobian_ofAlgEquiv

Modification history

2025-12-21 17:00
Mathlib/RingTheory/Extension/Presentation/Submersive.lean
feat(RingTheory/Smooth/StandardSmooth): transport `IsStandardSmooth` along algebra isomorphisms (#32925)
Added Algebra.PreSubmersivePresentation.jacobian_ofAlgEquivView on Github →