Stability of finiteness conditions in commutative algebra

In this file we show that Algebra.FiniteType and Algebra.FinitePresentation are stable under base change.

theorem Algebra.FiniteType.baseChangeAux_surj {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] {σ : Type u_1} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(TensorProduct.map (AlgHom.id B B) f)

instance Algebra.FiniteType.baseChange {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [hfa : FiniteType R A] : FiniteType B (TensorProduct R B A)

instance Algebra.FinitePresentation.baseChange {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [FinitePresentation R A] : FinitePresentation B (TensorProduct R B A)