Documentation Verification Report

PartialFractions

📁 Source: Mathlib/Algebra/Polynomial/PartialFractions.lean

Statistics

Metric	Count
Definitions	0
Theorems `div_eq_quo_add_rem_div_add_rem_div`, `div_prod_eq_quo_add_sum_rem_div`, `eq_quo_mul_pow_add_sum_rem_mul_pow`, `eq_quo_mul_prod_add_sum_rem_mul_prod`, `eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow`, `mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse`, `quo_add_rem_div_add_rem_div_unique`, `quo_add_sum_rem_div_unique`, `quo_add_sum_rem_mul_pow_inverse_unique`, `quo_mul_pow_add_sum_rem_mul_pow_unique`, `quo_mul_prod_add_sum_rem_mul_prod_unique`, `quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique`, `div_eq_quo_add_rem_div_add_rem_div`, `div_eq_quo_add_sum_rem_div`	14
Total	14

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_eq_quo_add_rem_div_add_rem_div` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsCoprime` `Polynomial` `commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Algebra.cast` `commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd`	—	`Finset.coe_insert` `Finset.coe_singleton` `IsCoprime.symm` `div_prod_eq_quo_add_sum_rem_div` `Finset.mem_univ` `add_assoc` `Finset.prod_congr` `Finset.prod_insert` `Finset.prod_singleton` `Finset.sum_congr` `Finset.sum_insert` `Finset.sum_singleton`
`div_prod_eq_quo_add_sum_rem_div` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Algebra.cast` `commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Module.nontrivial` `DivisionRing.toNontrivial` `inv_mul_cancel₀` `Monic.ne_zero` `mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse` `Finset.sum_congr` `Finset.prod_congr` `div_eq_mul_inv` `Finset.prod_inv_distrib` `pow_one` `zero_add` `Fin.sum_univ_one`
`eq_quo_mul_pow_add_sum_rem_mul_pow` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `instAdd` `instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.univ` `Fin.fintype`	—	`Fin.isEmpty'` `pow_zero` `mul_one` `Finset.sum_congr` `Finset.univ_eq_empty` `add_zero` `Fin.snoc_last` `degree_modByMonic_lt` `Fin.snoc_castSucc` `Fin.sum_univ_castSucc` `add_rotate'` `add_assoc` `pow_succ'` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `mul_comm` `modByMonic_add_div`
`eq_quo_mul_prod_add_sum_rem_mul_prod` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `instAdd` `instMul` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.erase`	—	`Finset.cons_induction` `instIsEmptyFalse` `mul_one` `Finset.sum_congr` `Finset.prod_congr` `Finset.erase_eq_of_notMem` `add_zero` `Finset.forall_mem_cons` `Set.pairwise_insert` `Finset.coe_cons` `Function.update_self` `degree_modByMonic_lt` `Function.update_of_ne` `Finset.prod_cons` `Finset.sum_cons` `Finset.erase_cons` `add_mul` `Distrib.rightDistribClass` `add_add_add_comm` `mul_assoc` `add_comm` `mul_comm` `modByMonic_add_div` `add_assoc` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_mul` `Finset.sum_add_distrib` `Finset.erase_subset` `Finset.erase_cons_of_ne` `Finset.mul_prod_erase` `mul_right_comm` `mul_add` `Distrib.leftDistribClass`
`eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `instAdd` `instMul` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Fin.fintype` `Finset.erase`	—	`eq_quo_mul_prod_add_sum_rem_mul_prod` `Monic.pow` `Set.Pairwise.mono'` `IsCoprime.pow` `eq_quo_mul_pow_add_sum_rem_mul_pow` `add_mul` `Distrib.rightDistribClass` `add_assoc` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_mul` `Finset.sum_add_distrib` `Finset.sum_congr` `Finset.mul_prod_erase` `mul_assoc`
`mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `algebraMap` `Finset.prod` `CommRing.toCommMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `Fin.fintype`	—	`eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `Finset.prod_mul_distrib` `map_pow` `mul_pow` `mul_comm` `one_pow` `Finset.prod_congr` `Finset.prod_const_one` `mul_one` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `map_sum` `Finset.sum_mul` `Finset.sum_congr` `Equiv.sum_comp` `Fintype.sum_congr` `Fin.revPerm_apply` `Finset.prod_erase_mul` `mul_rotate'` `Finset.mem_of_mem_erase` `mul_left_comm` `pow_add`
`quo_add_rem_div_add_rem_div_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsCoprime` `Polynomial` `commSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Algebra.cast` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	—	`Finset.coe_insert` `Finset.coe_singleton` `IsCoprime.symm` `Finset.mem_univ` `quo_add_sum_rem_div_unique` `Finset.sum_congr` `Finset.sum_insert` `Finset.sum_singleton` `add_assoc`
`quo_add_sum_rem_div_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Algebra.cast` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	—	`Module.nontrivial` `DivisionRing.toNontrivial` `inv_mul_cancel₀` `Monic.ne_zero` `quo_add_sum_rem_mul_pow_inverse_unique` `Finset.sum_congr` `Fin.sum_univ_one` `zero_add` `pow_one`
`quo_add_sum_rem_mul_pow_inverse_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `Fin.fintype` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—	`add_mul` `Distrib.rightDistribClass` `Finset.sum_mul` `Finset.sum_congr` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_sum` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finset.prod_congr` `map_pow` `Equiv.sum_comp` `Fintype.sum_congr` `Fin.revPerm_apply` `Finset.mul_prod_erase` `mul_assoc` `mul_one` `one_pow` `mul_pow` `pow_add` `mul_right_comm` `one_mul` `quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique` `FaithfulSMul.algebraMap_injective`
`quo_mul_pow_add_sum_rem_mul_pow_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.univ` `Fin.fintype`	—	—	`pow_zero` `mul_one` `Finset.sum_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `add_zero` `Fin.snoc_castSucc` `mul_comm` `add_mul` `Distrib.rightDistribClass` `add_assoc` `mul_assoc` `pow_succ'` `add_rotate'` `Fin.sum_univ_castSucc` `Fin.snoc_last` `div_modByMonic_unique`
`quo_mul_prod_add_sum_rem_mul_prod_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `instAdd` `instMul` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.erase`	—	—	`Finset.cons_induction` `instIsEmptyFalse` `mul_one` `Finset.sum_congr` `Finset.prod_congr` `Finset.erase_eq_of_notMem` `add_zero` `Finset.prod_cons` `IsCoprime.mul_right_iff` `Finset.cons_eq_insert` `Finset.cons.congr_simp` `Finset.coe_insert` `Finset.mem_cons_of_mem` `Set.Pairwise.mono` `SetLike.coe_mono` `instIsConcreteLE` `Finset.cons_subset_cons` `Finset.subset_cons` `IsCoprime.dvd_of_dvd_mul_right` `dvd_mul_right` `sub_eq_zero` `neg_add_eq_sub` `neg_mul` `neg_sub` `mul_sub` `sub_mul` `add_sub_add_comm` `mul_add` `Distrib.leftDistribClass` `add_left_comm` `mul_left_comm` `Finset.erase_subset` `Finset.erase_cons_of_ne` `Finset.erase_cons` `Finset.sum_cons` `IsCoprime.dvd_of_dvd_mul_left` `IsCoprime.symm` `dvd_mul_left` `Finset.sum_sub_distrib` `eq_sub_iff_add_eq'` `mul_assoc` `LE.le.trans_lt` `degree_sub_le` `max_lt` `Finset.forall_mem_cons` `Function.mtr` `Monic.not_dvd_of_degree_lt` `monic_prod_of_monic` `degree_sum_le` `Finset.sup_lt_iff` `bot_lt_iff_ne_bot` `degree_ne_bot` `Monic.ne_zero_of_polynomial_ne` `lt_irrefl` `Finset.mul_prod_erase` `mul_comm` `Monic.degree_mul` `degree_mul_le` `Finset.mem_of_mem_erase` `add_comm` `WithBot.add_lt_add_iff_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Monic.mul_right_eq_zero_iff` `Monic.mul` `mul_rotate` `neg_eq_zero` `zero_sub` `MulZeroClass.mul_zero`
`quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique` 📖	—	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `commSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `instAdd` `instMul` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Fin.fintype` `Finset.erase`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `LE.le.trans_lt` `degree_sum_le` `Finset.sup_lt_iff` `bot_lt_iff_ne_bot` `degree_ne_bot` `Monic.ne_zero` `Monic.pow` `degree_mul_le` `degree_eq_natDegree` `Monic.natDegree_pow` `Fin.neZero` `Nat.cast_add` `WithBot.add_lt_add_of_lt_of_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `WithBot.natCast_ne_bot` `Nat.cast_le` `WithBot.addLeftMono` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `quo_mul_prod_add_sum_rem_mul_prod_unique` `Set.Pairwise.imp` `IsCoprime.pow` `Finset.sum_congr` `quo_mul_pow_add_sum_rem_mul_pow_unique`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_eq_quo_add_rem_div_add_rem_div` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsCoprime` `Polynomial` `Polynomial.commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Algebra.cast` `Polynomial.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd`	—	`Polynomial.div_eq_quo_add_rem_div_add_rem_div`
`div_eq_quo_add_sum_rem_div` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCoprime` `Polynomial` `Polynomial.commSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Algebra.cast` `Polynomial.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Polynomial.div_prod_eq_quo_add_sum_rem_div`

---

← Back to Index