Theorems · Definition · commutative algebra
xInTermsOfW
(p : ℕ) → (R : Type u_1) → [inst : CommRing R] → [Invertible ↑p] → ℕ → MvPolynomial ℕ R
The xInTermsOfW p R n is the polynomial on the basis of Witt polynomials
that corresponds to the ordinary X n.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingInvertible
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- MvPolynomialstatement and proof · cited by 2,140
- MvPolynomial.Xproof · cited by 552
- Invertiblestatement and proof · cited by 549
- MvPolynomial.Cproof · cited by 400
- Invertible.invOfproof · cited by 268
Cited by23
Results whose statement or proof uses this declaration.
- wittStructureRatproof · cited by 12
- xInTermsOfW_eqstatement and proof · cited by 7
- xInTermsOfW_zerostatement and proof · cited by 7
- wittStructureRat_propproof · cited by 4
- bind₁_wittPolynomial_xInTermsOfWstatement and proof · cited by 3
- WittVector.frobeniusPolyRatproof · cited by 3
- bind₁_xInTermsOfW_wittPolynomialstatement and proof · cited by 2
- xInTermsOfW_auxstatement and proof · cited by 2
- constantCoeff_xInTermsOfWstatement and proof · cited by 2
- WittVector.wittZero_eq_zeroproof · cited by 1
- WittVector.bind₁_frobeniusPolyRat_wittPolynomialproof · cited by 1
- wittStructureRat_existsUniqueproof · cited by 1