Theorems · Theorem · field theory
Polynomial.modByMonic_add_div
∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p %ₘ q + q * (p /ₘ q) = p- Defined in
- Mathlib.Algebra.Polynomial.Div
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- Polynomial.modByMonicstatement · cited by 82
- Polynomial.divByMonicstatement · cited by 77
- eq_sub_iff_add_eqproof · cited by 65
- Polynomial.modByMonic_eq_sub_mul_divproof · cited by 13
Cited by25
Results whose statement or proof uses this declaration.
- Polynomial.modByMonic_eq_zero_iff_dvdproof · cited by 15
- Polynomial.div_modByMonic_uniqueproof · cited by 12
- Polynomial.divByMonic_eq_zero_iffproof · cited by 7
- Polynomial.mul_divByMonic_eq_iff_isRootproof · cited by 5
- Polynomial.degree_add_divByMonicproof · cited by 4
- Polynomial.resultant_X_sub_C_leftproof · cited by 3
- Submodule.span_range_natDegree_eq_adjoinproof · cited by 3
- Polynomial.add_modByMonicproof · cited by 3
- Polynomial.modByMonic_eq_of_dvd_subproof · cited by 3
- Polynomial.pow_mul_divByMonic_rootMultiplicity_eqproof · cited by 3
- Polynomial.map_mod_divByMonicproof · cited by 2
- PowerBasis.repr_gen_pow_isIntegralproof · cited by 2