feat(AlgebraicGeometry/AffineSpace): affine space over an integral base is integral#39665

justus-springer wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/AffineSpace_isIntegraljustus-springer/mathlib4:justus/AffineSpace_isIntegralCopy head branch name to clipboard