Theorems · Theorem · commutative algebra
Ideal.top_mul
∀ {R : Type u} [inst : Semiring R] (I : Ideal R), ⊤ * I = I- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 72 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.
Cites4
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
- Top.topstatement · cited by 9,680
- Idealstatement and proof · cited by 4,748
- Submodule.top_smulproof · cited by 11
Cited by10
Results whose statement or proof uses this declaration.
- Ideal.isCoprime_iff_codisjointproof · cited by 6
- PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal'proof · cited by 2
- ClassGroup.mk_eq_one_of_coe_idealproof · cited by 2
- Ideal.top_powproof · cited by 2
- Algebra.IsLocalIso.transproof · cited by 1
- Submodule.exists_eq_colon_of_mem_minimalPrimesproof · cited by 1
- Ideal.spanNorm_mul_of_bot_or_topproof · cited by 1
- WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdealproof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.top_mulproof · cited by 0
- PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_idealproof · cited by 0