English
IsAlgebraic R z is equivalent to the existence of a nonzero y with IsIntegral R (y • z), under IsReduced R.
Русский
IsAlgebraic R z эквивалентно существованию не нулевого y, такому что IsIntegral R (y • z), при условии, что R is IsReduced.
LaTeX
$$IsReduced R ⇒ (IsAlgebraic R z \iff ∃ y ≠ (0 : R), IsIntegral R (instHSMul.hSMul y z))$$
Lean4
protected theorem add : 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 b0 a0, ?_⟩
rw [smul_add, mul_smul, mul_comm, mul_smul]
exact (int_a.smul _).add (int_b.smul _)
