Theorems · Theorem · number theory
WittVector.RecursionMain.succNthDefiningPoly_degree
∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] [IsDomain k] (n : ℕ)
(a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k),
a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p- Cited by
- 1 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
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
- Polynomialproof · cited by 5,681
- mul_oneproof · cited by 3,885
- Factstatement and proof · cited by 2,726
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- IsDomainstatement and proof · cited by 2,196
- Nat.Primestatement and proof · cited by 2,059
- Nat.cast_zeroproof · cited by 1,870
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
Cited by1
Results whose statement or proof uses this declaration.
- WittVector.RecursionMain.root_existsproof · cited by 1