Theorem Algebra.Smooth.DescentAux.fg_subalgebra

Modification history

2026-01-07 13:28
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
feat(RingTheory): noetherian model for etale algebras (#32837)
Added Algebra.Smooth.DescentAux.fg_subalgebraView on Github →