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

[justus-springer]

Prove that AffineSpace inherits the properties IrreducibleSpace, IsReduced and IsIntegral from its base.

Also clean up a few variables, that were used very scarcely. These were causing weird issues in these new instances, where they would be automatically included.

---

[github-actions]

PR summary 7a9d34c18d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.AffineSpace	2457	2484	+27 (+1.10%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.AffineSpace	27

---

Declarations diff

+ instance : GeometricallyIrreducible (𝔸(n; S) ↘ S) := by
+ instance [IrreducibleSpace S] : IrreducibleSpace 𝔸(n; S)
+ instance [IsIntegral S] : IsIntegral 𝔸(n; S) := isIntegral_of_irreducibleSpace_of_isReduced _
+ instance [h : IsReduced S] : IsReduced 𝔸(n; S) := by
+ instance {X : Scheme.{max u v}} [X.Over S] (v : n → Γ(X, ⊤)) :
- instance (v : n → Γ(X, ⊤)) : (homOfVector (X ↘ S) v).IsOver S

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.