Theorem AlgebraicGeometry.smooth_of_grpObj

Modification history

2026-05-08 17:18
Mathlib/AlgebraicGeometry/Group/Smooth.lean
feat(AlgebraicGeometry): geometrically reduced group scheme over a field is smooth (#37988)
Added AlgebraicGeometry.smooth_of_grpObjView on Github →