irrational): add a lemma to deduce nat_degree from irrational root (#4349)

Commit

5 years ago

feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349) This PR is splitted from #4301 . Co-authored-by: Johan Commelin <johan@commelin.net>

References

#4925 - Make prime-avoidance branch build

Author

jjaassoonn

Parents

ddaa325e

mathlib d5834ee3 - feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349)

mathlib
d5834ee3 - feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349)