Theorem AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed

Modification history

2026-05-08 17:18
Mathlib/AlgebraicGeometry/Group/Smooth.lean
feat(AlgebraicGeometry): geometrically reduced group scheme over a field is smooth (#37988)
Deleted AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosedView on Github →
2026-02-13 12:38
Mathlib/AlgebraicGeometry/Group/Smooth.lean
feat(AlgebraicGeometry): reduced group schemes over algclosed fields are smooth (#35166)
Added AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosedView on Github →