Theorems · Theorem · commutative algebra
AddSubmonoid.smul_mem_smul
∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
{M : AddSubmonoid R} {N : AddSubmonoid A} {m : R} {n : A}, m ∈ M → n ∈ N → m • n ∈ M • N- Defined in
- Mathlib.Algebra.Ring.Submonoid.Pointwise
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddMonoidstatement and proof · cited by 2,864
- AddSubmonoidstatement and proof · cited by 1,178
- le_iSupproof · cited by 207
- DistribSMulstatement and proof · cited by 117
- AddSubmonoid.mapproof · cited by 99
- DistribSMul.toAddMonoidHomproof · cited by 20
- AddSubmonoid.smulstatement · cited by 11
Cited by8
Results whose statement or proof uses this declaration.
- Submodule.smul_mem_smulproof · cited by 32
- AddSubmonoid.smul_leproof · cited by 8
- AddSubmonoid.mul_mem_mulproof · cited by 4
- AddSubmonoid.smul_le_smulproof · cited by 4
- AddSubmonoid.addSubmonoid_smul_supproof · cited by 2
- AddSubmonoid.smul_iSupproof · cited by 2
- AddSubmonoid.smul_subset_smulproof · cited by 2
- IsHausdorff.of_mapproof · cited by 0