English
If y is a non-zero-divisor in S, y is algebraic over R, and y z is algebraic over R, then z is algebraic over R.
Русский
Если y не является нулевым делителем в S, y алгебраичен над R и y z алгебраичен над R, то z алгебраичен над R.
LaTeX
$$$[NoZeroDivisors R] \\Rightarrow (hy : y \\in \\text{nonZeroDivisors}(S)) \\to (\\text{alg}(R,y)) \\to (\\text{alg}(R,yz)) \\Rightarrow \\text{alg}(R,z)$$$
Lean4
theorem of_mul [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S) (alg_y : IsAlgebraic R y)
(alg_yz : IsAlgebraic R (y * z)) : IsAlgebraic R z :=
by
have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
rw [mul_right_comm, eq, ← Algebra.smul_def] at this
exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)
