Theorems · Theorem · commutative algebra
Ideal.mul_le
∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R}, I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Idealstatement and proof · cited by 4,748
- Submodule.smul_leproof · cited by 20
Cited by11
Results whose statement or proof uses this declaration.
- Ideal.mul_topproof · cited by 42
- Ideal.mul_le_rightproof · cited by 20
- Ideal.mul_le_leftproof · cited by 19
- Ideal.mul_le_infproof · cited by 10
- Ideal.map_mulproof · cited by 9
- Ideal.IsPrime.mul_leproof · cited by 8
- ClassGroup.exists_mk0_eq_mk0proof · cited by 1
- Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHomproof · cited by 1
- Ideal.leadingCoeff_mul_leproof · cited by 1
- IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipalproof · cited by 1
- Ideal.mul_commproof · cited by 0