of_smul — Mathlib

English

If y is a non-zero divisor in R and IsIntegral R (y • z), then z is algebraic over R.

Русский

Если y — нулевой делитель не образующий нули, и y z интегрально над R, то z алгебраическая над R.

LaTeX

$$$y \in\mathrm{nonZeroDivisors}(R) \Rightarrow IsIntegral(R, y \cdot z) \Rightarrow Algebra.IsAlgebraic R z$$$

Lean4

theorem of_smul {y : R} (hy : y ∈ nonZeroDivisors R) (h : IsAlgebraic R (y • z)) : IsAlgebraic R z :=
  have ⟨p, hp, eval0⟩ := h
  ⟨_, mt (comp_C_mul_X_eq_zero_iff hy).mp hp, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩

Похожие утверждения