Commit 2026-05-08 17:18 27aad96d

View on Github →

feat(AlgebraicGeometry): geometrically reduced group scheme over a field is smooth (#37988)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Group/Smooth.lean

added theorem AlgebraicGeometry.smooth_of_grpObj

deleted theorem AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed

Modified Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean

added theorem AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat

Created Mathlib/AlgebraicGeometry/Morphisms/LocalFlatDescent.lean