Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat_degree_gt_one_of_irrational_root

Modification history

2020-10-27 19:53
src/data/real/irrational.lean
refactor(data/polynomial): use `linear_map` for `monomial`, review `degree` (#4784)
Deleted nat_degree_gt_one_of_irrational_rootView on Github →
2020-10-01 17:37
src/data/real/irrational.lean
feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349) …
Added nat_degree_gt_one_of_irrational_rootView on Github →