Mathlib v3 is deprecated. Go to Mathlib v4

Theorem one_lt_nat_degree_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)
Added one_lt_nat_degree_of_irrational_rootView on Github →