Commit 2024-02-06 16:43 229b0bad

View on Github →

feat: define Newton's method and prove decomposition as nilpotent + root (#10284) This is just a modified version of the code provided by Antoine Chambert-Loir here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/jordan-chevalley.20decomposition/near/411402670

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Newton.lean

added theorem Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap

added theorem Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero

added theorem Polynomial.isFixedPt_newtonMap_of_aeval_eq_zero

added theorem Polynomial.isFixedPt_newtonMap_of_isUnit_iff

added theorem Polynomial.isNilpotent_iterate_newtonMap_sub_of_isNilpotent

added def Polynomial.newtonMap

added theorem Polynomial.newtonMap_apply

added theorem Polynomial.newtonMap_apply_of_isUnit

added theorem Polynomial.newtonMap_apply_of_not_isUnit

Modified Mathlib/RingTheory/Nilpotent.lean

deleted theorem Commute.IsNilpotent.add_isUnit

added theorem IsNilpotent.isUnit_add_left_of_commute

added theorem IsNilpotent.isUnit_add_one

added theorem IsNilpotent.isUnit_add_right_of_commute

added theorem IsNilpotent.isUnit_one_add

added theorem IsNilpotent.isUnit_one_sub

added theorem IsNilpotent.isUnit_sub_one

deleted theorem IsNilpotent.sub_one_isUnit

added theorem IsUnit.isNilpotent_mul_unit_of_commute_iff

added theorem IsUnit.isNilpotent_unit_mul_of_commute_iff

Modified Mathlib/RingTheory/Polynomial/IrreducibleRing.lean

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

added theorem Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub

added theorem Polynomial.isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub

Modified Mathlib/RingTheory/Polynomial/Tower.lean

added theorem Polynomial.eval_map_algebraMap