English
If the numerator of a fractional ideal I is zero and the ambient structure has no zero smul divisors, and 0 is not in S, then I = 0.
Русский
Если числитель дробного идеала I равен нулю и окружение не содержит нулевых делителей, и 0 не принадлежит S, тогда I = 0.
LaTeX
$$$(I.num = \bot) \Rightarrow I = 0 \\text{ provided } 0 \notin S \text{ and NoZeroSMulDivisors}(R,P)$$$
Lean4
theorem zero_of_num_eq_bot [NoZeroSMulDivisors R P] (hS : 0 ∉ S) {I : FractionalIdeal S P} (hI : I.num = ⊥) : I = 0 :=
by
rw [← coeToSubmodule_eq_bot, eq_bot_iff]
intro x hx
suffices (den I : R) • x = 0 from (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)
have h_eq : I.den • (I : Submodule R P) = ⊥ := by rw [den_mul_self_eq_num, hI, Submodule.map_bot]
exact (Submodule.eq_bot_iff _).mp h_eq (den I • x) ⟨x, hx, rfl⟩
