mul — Mathlib

English

If y ∈ R is not nilpotent and y • z is integral over R, then z is algebraic over R.

Русский

Если y ∈ R не нильпотентно и y • z интегрально над R, тогда z алгебраическая над R.

LaTeX

$${y : R} (hy : ¬IsNilpotent y) (h : IsIntegral R (y • z)) : IsAlgebraic R z$$

Lean4

protected theorem mul : IsAlgebraic R (a * b) :=
  by
  have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
  have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
  refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩
  simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]
  exact int_a.mul int_b

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