Theorems · Theorem · field theory
Polynomial.natDegree_pow
∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ), (p ^ n).natDegree = n * p.natDegree- Defined in
- Mathlib.Algebra.Polynomial.Degree.Domain
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringNoZeroDivisors
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.
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement and proof · cited by 5,681
- MulZeroClass.mul_zeroproof · cited by 2,091
- eq_or_neproof · cited by 1,117
- Polynomial.natDegreestatement and proof · cited by 1,105
- pow_zeroproof · cited by 1,094
- NoZeroDivisorsstatement and proof · cited by 545
- Polynomial.leadingCoeffproof · cited by 498
- zero_powproof · cited by 361
- pow_ne_zeroproof · cited by 208
- Polynomial.leadingCoeff_eq_zeroproof · cited by 55
- Polynomial.natDegree_oneproof · cited by 43
Cited by11
Results whose statement or proof uses this declaration.
- IsPurelyInseparable.elemExponent_le_of_pow_memproof · cited by 3
- X_pow_sub_C_irreducible_of_oddproof · cited by 3
- FiniteField.orderOf_frobeniusAlgHomproof · cited by 3
- IsRealClosed.exists_eq_pow_of_oddproof · cited by 2
- IsPurelyInseparable.minpoly_natDegree_eqproof · cited by 2
- Complex.isOpenQuotientMap_powproof · cited by 1
- sum_smul_minpolyDiv_eq_X_powproof · cited by 1
- Polynomial.X_pow_sub_C_separable_iffproof · cited by 1
- Polynomial.aeval_sumIDeriv_of_posproof · cited by 1
- LindemannWeierstrass.exp_polynomial_approxproof · cited by 0