Theorems · Definition · commutative algebra
AddSubmonoid.mul
{R : Type u_2} → [inst : NonUnitalNonAssocSemiring R] → Mul (AddSubmonoid R)Multiplication of additive submonoids of a semiring R. The additive submonoid S * T is the
smallest R-submodule of R containing the elements s * t for s ∈ S and t ∈ T.
- Defined in
- Mathlib.Algebra.Ring.Submonoid.Pointwise
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonUnitalNonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- iSupproof · cited by 2,415
- AddSubmonoidstatement and proof · cited by 1,178
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- AddSubmonoid.mapproof · cited by 99
- AddMonoidHom.mulproof · cited by 7
Cited by19
Results whose statement or proof uses this declaration.
- AddSubmonoid.mul_lestatement · cited by 5
- AddSubmonoid.mul_mem_mulstatement · cited by 4
- AddSubmonoid.mul_le_mul_leftstatement · cited by 2
- AddSubmonoid.mul_comm_of_commutestatement · cited by 1
- Submodule.mul_toAddSubmonoidstatement · cited by 1
- AddSubmonoid.closure_mul_closurestatement · cited by 1
- AddSubmonoid.mul_botstatement · cited by 0
- AddSubmonoid.hasDistribNegstatement · cited by 0
- AddSubmonoid.mul_eq_closure_mul_setstatement · cited by 0
- AddSubmonoid.mul_iSupstatement · cited by 0
- AddSubmonoid.mul_induction_onstatement · cited by 0
- AddSubmonoid.mul_le_mulstatement · cited by 0