Theorems · Theorem · commutative algebra
wittPolynomial_eq_sum_C_mul_X_pow
∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] (n : ℕ), wittPolynomial p R n = ∑ i ∈ Finset.range (n + 1), MvPolynomial.C (↑p ^ i) * MvPolynomial.X i ^ p ^ (n - i)
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- RingHomstatement · cited by 10,189
- Finsuppstatement · cited by 5,255
- Finset.sumstatement · cited by 5,195
- Finset.sum_congrproof · cited by 2,323
- MvPolynomialstatement and proof · cited by 2,140
- Finset.rangestatement and proof · cited by 1,341
- pow_zeroproof · cited by 1,094
- MvPolynomial.Xstatement and proof · cited by 552
- MvPolynomial.Cstatement and proof · cited by 400
- wittPolynomialstatement · cited by 54
Cited by8
Results whose statement or proof uses this declaration.
- bind₁_wittPolynomial_xInTermsOfWproof · cited by 3
- WittVector.select_add_select_notproof · cited by 2
- bind₁_xInTermsOfW_wittPolynomialproof · cited by 2
- WittVector.map_frobeniusPolyproof · cited by 1
- wittPolynomial_zmod_selfproof · cited by 1
- WittVector.peval_polyOfInterestproof · cited by 1
- wittPolynomial_oneproof · cited by 0
- WittVector.bind₁_onePoly_wittPolynomialproof · cited by 0