Def Algebra.Smooth.DescentAux.subalgebra

Modification history

2026-07-24 07:15
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
chore: add missing `noncomputable` (#41446) …
Deleted Algebra.Smooth.DescentAux.subalgebraView on Github →
2025-12-09 15:53
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
feat(RingTheory): smooth algebras have smooth Noetherian models (#25143) …
Added Algebra.Smooth.DescentAux.subalgebraView on Github →