iff_exists_smul_integral — Mathlib

English

For NoZeroDivisors, IsAlgebraic K z is equivalent to the existence of y ≠ 0 with IsIntegral R (y • z).

Русский

Для NoZeroDivisors: IsAlgebraic K z эквивалентно существованию y ≠ 0 с IsIntegral R (y • z).

LaTeX

$$IsReduced R \Rightarrow (IsAlgebraic R z \iff ∃ y ≠ (0 : R), IsIntegral R (y \cdot z))$$

Lean4

theorem iff_exists_smul_integral [IsReduced R] : IsAlgebraic R z ↔ ∃ y ≠ (0 : R), IsIntegral R (y • z) :=
  ⟨(exists_integral_multiple ·), fun ⟨_, hy, int⟩ ↦ of_smul_isIntegral (by rwa [isNilpotent_iff_eq_zero]) int⟩

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