Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 10:17 13453191

View on Github →

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

Estimated changes