English
If ha is algebraic over R for a, and s ∈ S, then ta is algebraic over S for the tensor product; more precisely, IsAlgebraic S (s ⊗ₜ[R] a).
Русский
Если a алгебраический над R, то при тензорном произведении над R с s ∈ S алгебраичность над S сохраняется: IsAlgebraic S (s ⊗ₜ[R] a).
LaTeX
$$IsAlgebraic.smul_isInt? (tmul) [FaithfulSMul R S] : IsAlgebraic S (s ⊗ₜ[R] a)$$
Lean4
theorem tmul [FaithfulSMul R S] : IsAlgebraic S (s ⊗ₜ[R] a) :=
by
rw [← mul_one s, ← smul_eq_mul, ← TensorProduct.smul_tmul']
have ⟨p, h, eval0⟩ := ha
refine
.smul ⟨p.map (algebraMap R S), (Polynomial.map_ne_zero_iff <| FaithfulSMul.algebraMap_injective ..).mpr h, ?_⟩ _
rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A), ←
map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
