Theorem Algebra.Smooth.DescentAux.exists_kerSquareLift_comp_eq_id

Modification history

2025-12-09 15:53
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
feat(RingTheory): smooth algebras have smooth Noetherian models (#25143) …
Added Algebra.Smooth.DescentAux.exists_kerSquareLift_comp_eq_idView on Github →