Commit 2026-09-13 16:56 8d52ea9a

View on Github →

feat(AlgebraicGeometry/AffineSpace): affine space is smooth (#39710) Show that affine space 𝔸(n; S) is smooth over S (or relative dimension Nat.card n) . Note that this replaces the the LocallyOfFinitePresentation instance, as it can be inferred automatically from smoothness (instLocallyOfFinitePresentationOfSmooth).

depends on: #39709

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

added theorem AlgebraicGeometry.AffineSpace.smoothOfRelativeDimension_of_card_eq

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

deleted theorem AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange