Documentation Verification Report

Newton

📁 Source: Mathlib/Dynamics/Newton.lean

Statistics

Metric	Count
Definitions `newtonMap`	1
Theorems `aeval_pow_two_pow_dvd_aeval_iterate_newtonMap`, `existsUnique_nilpotent_sub_and_aeval_eq_zero`, `isFixedPt_newtonMap_of_aeval_eq_zero`, `isFixedPt_newtonMap_of_isUnit_iff`, `isNilpotent_iterate_newtonMap_sub_of_isNilpotent`, `newtonMap_apply`, `newtonMap_apply_of_isUnit`, `newtonMap_apply_of_not_isUnit`	8
Total	9

Polynomial

Definitions

Name	Category	Theorems
`newtonMap` 📖	CompOp	7 math math: `isFixedPt_newtonMap_of_isUnit_iff`, `aeval_pow_two_pow_dvd_aeval_iterate_newtonMap`, `isNilpotent_iterate_newtonMap_sub_of_isNilpotent`, `newtonMap_apply_of_isUnit`, `newtonMap_apply_of_not_isUnit`, `newtonMap_apply`, `isFixedPt_newtonMap_of_aeval_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_pow_two_pow_dvd_aeval_iterate_newtonMap` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `IsUnit` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Nat.instMonoid` `Nat.iterate` `newtonMap`	—	`pow_zero` `pow_one` `Function.iterate_succ'` `newtonMap_apply` `sub_eq_add_neg` `neg_mul_eq_neg_mul` `eval_map_algebraMap` `dvd_add` `Distrib.leftDistribClass` `isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub` `isNilpotent_iterate_newtonMap_sub_of_isNilpotent` `derivative_map` `mul_assoc` `mul_neg` `Ring.mul_inverse_cancel` `neg_mul` `one_mul` `add_neg_cancel` `dvd_zero` `dvd_mul_of_dvd_right` `Nat.instAtLeastTwoHAddOfNat` `Even.neg_pow` `even_two` `mul_pow` `pow_succ` `pow_mul` `pow_dvd_pow_of_dvd`
`existsUnique_nilpotent_sub_and_aeval_eq_zero` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `IsUnit` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	`ExistsUnique` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`neg_sub` `existsUnique_of_exists_of_unique` `isNilpotent_iterate_newtonMap_sub_of_isNilpotent` `zero_dvd_iff` `pow_eq_zero_of_le` `LT.lt.le` `aeval_pow_two_pow_dvd_aeval_iterate_newtonMap` `isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub` `sub_sub_sub_cancel_right` `IsNilpotent.isUnit_add_left_of_commute` `Commute.isNilpotent_mul_left` `Commute.all` `Commute.isNilpotent_sub` `sub_eq_zero` `IsUnit.mul_right_eq_zero` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `pow_two` `zero_add` `add_sub_cancel` `eval_map_algebraMap` `derivative_map`
`isFixedPt_newtonMap_of_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Function.IsFixedPt` `newtonMap`	—	`Function.IsFixedPt.eq_1` `newtonMap_apply` `MulZeroClass.mul_zero` `sub_zero`
`isFixedPt_newtonMap_of_isUnit_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	`Function.IsFixedPt` `newtonMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Function.IsFixedPt.eq_1` `newtonMap_apply` `sub_eq_self` `Ring.inverse_mul_eq_iff_eq_mul` `MulZeroClass.mul_zero`
`isNilpotent_iterate_newtonMap_sub_of_isNilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.iterate` `newtonMap`	—	`sub_self` `Function.iterate_succ'` `newtonMap_apply` `sub_right_comm` `Commute.isNilpotent_sub` `Commute.all` `Commute.isNilpotent_mul_left` `sub_add_cancel` `Commute.isNilpotent_add` `isNilpotent_aeval_sub_of_isNilpotent_sub`
`newtonMap_apply` 📖	mathematical	—	`newtonMap` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.inverse` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	—	—
`newtonMap_apply_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	`newtonMap` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Units.val` `Units` `Units.instInv` `IsUnit.unit`	—	—
`newtonMap_apply_of_not_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	`newtonMap`	—	`MulZeroClass.zero_mul` `sub_zero`

---

← Back to Index