Theorems · Theorem · group theory
multiset_prod_mem
∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [SubmonoidClass B M]
(m : Multiset M), (∀ a ∈ m, a ∈ S) → m.prod ∈ SProduct of a multiset of elements in a submonoid of a CommMonoid is in the submonoid.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 60 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.
- Multisetstatement and proof · cited by 2,627
- CommMonoidstatement and proof · cited by 2,264
- SetLikestatement and proof · cited by 1,084
- Multiset.mapproof · cited by 876
- Multiset.prodstatement and proof · cited by 528
- SubmonoidClassstatement and proof · cited by 60
- Subtype.coe_propproof · cited by 42
- SubmonoidClass.coe_multiset_prodproof · cited by 2
Cited by11
Results whose statement or proof uses this declaration.
- prod_memproof · cited by 16
- Polynomial.Splits.multisetProdproof · cited by 6
- Submonoid.multiset_prod_memproof · cited by 3
- Subring.multiset_prod_memproof · cited by 1
- PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subsetproof · cited by 1
- Subalgebra.multiset_prod_memproof · cited by 1
- IntermediateField.multiset_prod_memproof · cited by 0
- Subfield.multiset_prod_memproof · cited by 0
- HasCompactMulSupport.multiset_prodproof · cited by 0
- Subsemiring.multiset_prod_memproof · cited by 0
- Subgroup.multiset_prod_memproof · cited by 0