Theorem Algebra.isReduced_of_isGeometricallyReduced

Modification history

2025-11-13 13:13
Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean
feat: define geometrically reduced algebras (#27400) …
Added Algebra.isReduced_of_isGeometricallyReducedView on Github →