Commit 2024-11-16 06:58 aa5b6a4a

View on Github →

feat(AlgebraicGeometry): define affine n-space (#18837)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.ext_of_isAffine

Created Mathlib/AlgebraicGeometry/AffineSpace.lean

added def AlgebraicGeometry.AffineSpace.SpecIso

added theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_app_top

added theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_over

added theorem AlgebraicGeometry.AffineSpace.comp_homOfVector

added def AlgebraicGeometry.AffineSpace.coord

added def AlgebraicGeometry.AffineSpace.functor

added def AlgebraicGeometry.AffineSpace.homOfVector

added theorem AlgebraicGeometry.AffineSpace.homOfVector_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.homOfVector_over

added theorem AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly

added def AlgebraicGeometry.AffineSpace.homOverEquiv

added theorem AlgebraicGeometry.AffineSpace.hom_ext

added def AlgebraicGeometry.AffineSpace.isoOfIsAffine

added theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_app_top

added theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over

added def AlgebraicGeometry.AffineSpace.map

added def AlgebraicGeometry.AffineSpace.mapSpecMap

added theorem AlgebraicGeometry.AffineSpace.map_Spec_map

added theorem AlgebraicGeometry.AffineSpace.map_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.map_comp

added theorem AlgebraicGeometry.AffineSpace.map_id

added theorem AlgebraicGeometry.AffineSpace.map_over

added theorem AlgebraicGeometry.AffineSpace.map_reindex

added theorem AlgebraicGeometry.AffineSpace.of_mvPolynomial_int_ext

added def AlgebraicGeometry.AffineSpace.reindex

added theorem AlgebraicGeometry.AffineSpace.reindex_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.reindex_comp

added theorem AlgebraicGeometry.AffineSpace.reindex_id

added theorem AlgebraicGeometry.AffineSpace.reindex_over

added def AlgebraicGeometry.AffineSpace.toSpecMvPoly

added def AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv

added theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp

added def AlgebraicGeometry.AffineSpace