irrational): add a proof that a transcendental real number is irrational (#6721)

Commit

4 years ago

feat(ring_theory/algebraic data/real/irrational): add a proof that a transcendental real number is irrational (#6721) Zulip: https://leanprover.zulipchat.com/#narrow/stream/263328-triage

Author

adomani

Parents

4b1d5886

mathlib 13453191 - feat(ring_theory/algebraic data/real/irrational): add a proof that a transcendental real number is irrational (#6721)

mathlib
13453191 - feat(ring_theory/algebraic data/real/irrational): add a proof that a transcendental real number is irrational (#6721)