Main results

The main results that the formalization.yaml of FormalFrontier/polynomial-root-stability lists under status.main_results at commit efade497, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration	Kind	Where	Note
IsKrasner.exists_pos_adjoin_rootSet_eq_of_monic_separable	theorem	PolynomialRootStability/Krasner.lean, line 565	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
IsKrasner.exists_pos_adjoin_rootSet_eq_of_separable_normalized	theorem	PolynomialRootStability/Normalization.lean, line 45	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
IsKrasner.exists_pos_adjoin_rootSet_eq_of_separable	theorem	PolynomialRootStability/Normalization.lean, line 214	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Valuation.map_eval_sub_eq_of_mul_map_sub_lt_map_derivative	theorem	PolynomialRootStability/Valuation.lean, line 163	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Valuation.map_derivative_eval_eq_of_mul_map_sub_lt_map_derivative	theorem	PolynomialRootStability/Valuation.lean, line 209	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Valuation.map_eval_sub_eval_eq_of_mul_map_sub_lt_map_derivative	theorem	PolynomialRootStability/Valuation.lean, line 220	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Valuation.injOn_eval_of_mul_map_sub_lt_map_derivative	theorem	PolynomialRootStability/Valuation.lean, line 245	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Polynomial.exists_root_tendsto_iterate_newtonMap	theorem	PolynomialRootStability/Newton.lean, line 261	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.
Polynomial.exists_factorization_of_supNorm_lt_resultant_sq	theorem	PolynomialRootStability/ResultantFactorization.lean, line 214	Sorry count 0. Axioms: propext, Classical.choice, Quot.sound.

Quoted from the main results in formalization.yaml of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.