class IsAffineAlgebra (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [Algebra k R] : Prop

• isDomain : IsDomain R
• finiteType : Algebra.FiniteType k R

noncomputable def algHomOfMaximalIdeal (k : Type u_4) {R : Type u_5} [Field k] [IsAlgClosed k] [CommRing R] [Algebra k R] [IsDomain R] [Algebra.FiniteType k R] (m : Ideal R) [hm : m.IsMaximal] : R →ₐ[k] k

theorem algHomOfMaximalIdeal_ker {k : Type u_1} [Field k] [IsAlgClosed k] {R : Type u_2} [CommRing R] [Algebra k R] [IsDomain R] [Algebra.FiniteType k R] (m : Ideal R) [hm : m.IsMaximal] (r : R) : (algHomOfMaximalIdeal k m) r = 0 ↔ r ∈ m

noncomputable def evalTensorMap {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {S : Type u_3} [CommRing S] [Algebra k S] (φ : R →ₐ[k] k) : TensorProduct k R S →ₐ[k] S

theorem coord_evalTensorMap {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {S : Type u_3} [CommRing S] [Algebra k S] {ι : Type u_4} (bS : Module.Basis ι k S) (φ : R →ₐ[k] k) (u : TensorProduct k R S) (i : ι) : (bS.repr ((evalTensorMap φ) u)) i = φ (((Algebra.TensorProduct.basisAux R bS) u) i)

theorem IsAffineAlgebra.tensorProduct {k : Type u_1} [Field k] [IsAlgClosed k] (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] [IsAffineAlgebra k R] [IsAffineAlgebra k S] : IsAffineAlgebra k (TensorProduct k R S)