Theorem Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero

Modification history

2024-12-18 19:47

Mathlib/Dynamics/Newton.lean

chore(Logic/ExistsUnique): amend usages of existsUnique to follow naming convention (#20028) …

Deleted Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero View on Github →

2024-02-06 16:43

Mathlib/Dynamics/Newton.lean

feat: define Newton's method and prove decomposition as nilpotent + root (#10284) …

Added Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero View on Github →