Theorem AlgebraicGeometry.AffineSpace.smoothOfRelativeDimension_of_card_eq

Modification history

2026-09-13 16:56
Mathlib/AlgebraicGeometry/AffineSpace.lean
feat(AlgebraicGeometry/AffineSpace): affine space is smooth (#39710) …
Added AlgebraicGeometry.AffineSpace.smoothOfRelativeDimension_of_card_eqView on Github →