Theorems · Theorem · field theory
Polynomial.expand_one
∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), (Polynomial.expand R 1) f = f- Defined in
- Mathlib.Algebra.Polynomial.Expand
- Cited by
- 10 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.
Cites14
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
- AlgHomstatement · cited by 3,236
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- map_mulproof · cited by 1,137
- map_addproof · cited by 964
- pow_oneproof · cited by 894
- map_powproof · cited by 503
- Polynomial.expandstatement and proof · cited by 90
- Polynomial.induction_onproof · cited by 23
Cited by10
Results whose statement or proof uses this declaration.
- Polynomial.natSepDegree_expandproof · cited by 4
- Irreducible.hasSeparableContractionproof · cited by 4
- Algebra.trace_eq_zero_of_not_isSeparableproof · cited by 2
- Polynomial.exists_separable_of_irreducibleproof · cited by 1
- Polynomial.map_iterateFrobenius_expandproof · cited by 1
- Polynomial.unique_separable_of_irreducibleproof · cited by 0
- Polynomial.expand_contract'proof · cited by 0
- Polynomial.IsSeparableContraction.degree_eqproof · cited by 0
- Polynomial.expand_powproof · cited by 0
- Polynomial.of_irreducible_expand_powproof · cited by 0