Def Algebra.SubmersivePresentation.ofHasCoeffs

Modification history

2026-01-07 13:28

Mathlib/RingTheory/Extension/Presentation/Core.lean

feat(RingTheory): noetherian model for etale algebras (#32837)

Added Algebra.SubmersivePresentation.ofHasCoeffs View on Github →