Theorems · Theorem · field theory
Polynomial.coeff_expand
∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
0 < p → ∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0- Defined in
- Mathlib.Algebra.Polynomial.Expand
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
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
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement and proof · cited by 5,681
- Finset.sumproof · cited by 5,195
- AlgHomstatement · cited by 3,236
- Finset.sum_congrproof · cited by 2,323
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- Polynomial.coeffstatement and proof · cited by 1,045
- Polynomial.supportproof · cited by 237
- Finset.sum_eq_zeroproof · cited by 139
- Finset.sum_eq_singleproof · cited by 98
Cited by11
Results whose statement or proof uses this declaration.
- Polynomial.natDegree_expandproof · cited by 7
- Polynomial.map_expandproof · cited by 7
- Polynomial.coeff_expand_mulproof · cited by 5
- Algebra.trace_eq_zero_of_not_isSeparableproof · cited by 2
- Polynomial.expand_contractproof · cited by 2
- exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_powproof · cited by 2
- Polynomial.isLocalHom_expandproof · cited by 2
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1
- Field.isAlgebraic_of_adjoin_eq_adjoinproof · cited by 1
- Polynomial.contract_mul_expandproof · cited by 1
- Polynomial.contract_expandproof · cited by 0