Def AlgebraicGeometry.Scheme.Hom.smoothLocus

Modification history

2026-02-13 12:38

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

feat(AlgebraicGeometry): reduced group schemes over algclosed fields are smooth (#35166)

Added AlgebraicGeometry.Scheme.Hom.smoothLocus View on Github →