Theorems · Theorem · group theory
Multiset.prod_replicate
∀ {M : Type u_3} [inst : CommMonoid M] (n : ℕ) (a : M), (Multiset.replicate n a).prod = a ^ n- Cited by
- 40 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- CommMonoid
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.
- CommMonoidstatement and proof · cited by 2,264
- Multiset.prodstatement · cited by 528
- Multiset.replicatestatement · cited by 88
- List.prod_replicateproof · cited by 29
Cited by40
Results whose statement or proof uses this declaration.
- Finset.prod_constproof · cited by 154
- Finset.prod_const_oneproof · cited by 100
- Ideal.irreducible_pow_supproof · cited by 5
- Polynomial.natDegree_multiset_prod_of_monicproof · cited by 4
- Height.mulHeight_oneproof · cited by 4
- IsDiscreteValuationRing.associated_pow_irreducibleproof · cited by 4
- Polynomial.resultant_eq_prod_evalproof · cited by 3
- Multiset.prod_X_add_C_eq_sum_esymmproof · cited by 3
- Polynomial.count_map_rootsproof · cited by 2
- Associates.factors_prime_powproof · cited by 2
- Height.max_mulHeightBound_zero_one_eq_oneproof · cited by 2
- Height.mulHeight_linearMap_apply_leproof · cited by 2