feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349)
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 <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib