Theorems · Theorem · commutative algebra
wittPolynomial_zmod_self
∀ (p n : ℕ), wittPolynomial p (ZMod (p ^ (n + 1))) (n + 1) = (MvPolynomial.expand p) (wittPolynomial p (ZMod (p ^ (n + 1))) n)
Over the ring ZMod (p^(n+1)), we produce the n+1st Witt polynomial
by expanding the nth Witt polynomial by p.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites33
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
- CommSemiringproof · cited by 10,911
- RingHomproof · cited by 10,189
- Finsuppstatement · cited by 5,255
- Finset.sumproof · cited by 5,195
- Algebra.algebraMapproof · cited by 4,706
- AlgHomstatement · cited by 3,236
- add_zeroproof · cited by 2,707
- Finset.sum_congrproof · cited by 2,323
- MvPolynomialstatement and proof · cited by 2,140
- MulZeroClass.zero_mulproof · cited by 1,625
- add_commproof · cited by 1,535
Cited by1
Results whose statement or proof uses this declaration.
- C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sumproof · cited by 1