Documentation Verification Report

DenomsClearable

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

Statistics

Metric	Count
Definitions `DenomsClearable`	1
Theorems `add`, `denomsClearable_C_mul_X_pow`, `denomsClearable_natDegree`, `denomsClearable_of_natDegree_le`, `denomsClearable_zero`, `one_le_pow_mul_abs_eval_div`	6
Total	7

DenomsClearable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`DenomsClearable`	`Polynomial` `Polynomial.instAdd`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Polynomial.map_add` `Polynomial.eval_add` `mul_add` `Distrib.leftDistribClass` `inv_unique` `mul_comm`

(root)

Definitions

Name	Category	Theorems
`DenomsClearable` 📖	MathDef	4 math math: `denomsClearable_zero`, `denomsClearable_natDegree`, `denomsClearable_of_natDegree_le`, `denomsClearable_C_mul_X_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denomsClearable_C_mul_X_pow` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`DenomsClearable` `Polynomial` `Polynomial.instMul` `Polynomial.semiring` `Polynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.X`	—	`Polynomial.C_mul_X_pow_eq_monomial` `Polynomial.map_monomial` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_C` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.eval_X` `mul_comm` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `mul_one` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `mul_left_comm` `mul_pow` `pow_add` `mul_assoc`
`denomsClearable_natDegree` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`DenomsClearable` `Polynomial.natDegree`	—	`denomsClearable_of_natDegree_le` `le_rfl`
`denomsClearable_of_natDegree_le` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Polynomial.natDegree`	`DenomsClearable`	—	`Polynomial.induction_with_natDegree_le` `denomsClearable_zero` `denomsClearable_C_mul_X_pow` `DenomsClearable.add`
`denomsClearable_zero` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`DenomsClearable` `Polynomial` `Polynomial.instZero`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.map_zero` `Polynomial.eval_zero` `MulZeroClass.mul_zero`
`one_le_pow_mul_abs_eval_div` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddGroupWithOne.toIntCast` `Polynomial.natDegree` `Int.instSemiring` `abs` `AddGroupWithOne.toAddGroup` `Polynomial.eval` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Polynomial.map` `CommSemiring.toSemiring` `Int.instCommSemiring` `algebraMap` `Ring.toIntAlgebra`	—	`denomsClearable_natDegree` `eq_intCast` `RingHom.instRingHomClass` `one_div_mul_cancel` `Int.cast_ne_zero` `IsStrictOrderedRing.toCharZero` `LT.lt.ne` `div_eq_mul_inv` `one_div` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Int.cast_pos` `NeZero.charZero_one` `abs_mul` `eq_one_div_of_mul_eq_one_left` `Int.cast_abs` `Int.cast_one` `Int.cast_le` `lt_add_iff_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `abs_pos` `zero_eq_mul` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `Int.cast_zero` `not_le` `le_of_eq` `Int.cast_eq_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors`

---

← Back to Index