K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : FiniteDimensional K { x // x ∈ E1 }
inst✝ : FiniteDimensional K { x // x ∈ E2 }
⊢ FiniteDimensional K { x // x ∈ AlgHom.range (Algebra.TensorProduct.productMap (val E1) (val E2)) }
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : FiniteDimensional K { x // x ∈ E1 }
inst✝ : FiniteDimensional K { x // x ∈ E2 }
⊢ FiniteDimensional K { x // x ∈ E1 ⊔ E2 }
rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]
no goals
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : FiniteDimensional K { x // x ∈ E1 }
inst✝ : FiniteDimensional K { x // x ∈ E2 }
⊢ FiniteDimensional K { x // x ∈ AlgHom.range (Algebra.TensorProduct.productMap (val E1) (val E2)) }
exact (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap.finiteDimensional_range