integralRep_mem_nonZeroDivisors — Mathlib

English

If a fractional ideal is nonzero, its integral representative lies in the nonzero divisors of R.

Русский

Если дробный идеал не нулевой, то его интегральный представитель принадлежит к множеству ненулевых делителей R.

LaTeX

$$$I \neq 0 \Rightarrow I_{\mathrm{num}} \in (\mathrm{Ideal}(R))^{0}$$$

Lean4

theorem integralRep_mem_nonZeroDivisors {I : FractionalIdeal R⁰ (FractionRing R)} (hI : I ≠ 0) : I.num ∈ (Ideal R)⁰ :=
  by rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]

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