Theorem AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat

Modification history

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