Theorems · Theorem · group theory
Finset.pow_eq_prod_const
∀ {M : Type u_4} [inst : CommMonoid M] (b : M) (n : ℕ), b ^ n = ∏ _k ∈ Finset.range n, b- Cited by
- 4 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.prodstatement · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finset.rangestatement · cited by 1,341
- Finset.prod_constproof · cited by 154
- Finset.card_rangeproof · cited by 108
Cited by4
Results whose statement or proof uses this declaration.
- MvPolynomial.totalDegree_powproof · cited by 1
- MvPowerSeries.monomial_powproof · cited by 1
- tendsto_factorial_div_pow_self_atTopproof · cited by 0
- MvPolynomial.degreeOf_pow_eqproof · cited by 0