English
Equivalence between a product of a spanSingleton and a coeIdeal and a product of spans of generators of I and J.
Русский
Эквивалентность между произведением spanSingleton и коэдиала и произведением span от генераторов I и J.
LaTeX
$$Iff (Eq (instHMul.hMul (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) z) (FractionalIdeal.coeIdeal I)) (FractionalIdeal.coeIdeal J)) (Eq (instHMul.hMul (Ideal.span (Set.instSingletonSet.singleton (IsLocalization.sec (nonZeroDivisors R₁) z).fst)) I) (instHMul.hMul (Ideal.span (Set.instSingletonSet.singleton (IsLocalization.sec (nonZeroDivisors R₁) z).snd.val)) J))$$
Lean4
theorem num_le (I : FractionalIdeal S P) : (I.num : FractionalIdeal S P) ≤ I :=
by
rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]
intro _ h
rw [← Algebra.smul_def]
exact Submodule.smul_mem _ _ h
