Mathlib Map

Theorems · Theorem · number theory

Rat.not_irrational

∀ (q : ℚ), ¬Irrational ↑q
Defined in
Mathlib.NumberTheory.Real.Irrational
Cited by
3 results in Mathlib
Foundations
Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Irrational.of_ratCast_add · cited by 5Irrational.of_ratCast_addIrrational.of_mul_ratCast · cited by 3Irrational.of_mul_ratCastIrrational.of_div_ratCast · cited by 0Irrational.of_div_ratCastReal · cited by 25697RealIrrational · cited by 139IrrationalRat.not_irrationalCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement · cited by 25,697
  • Irrationalstatement and proof · cited by 139

Cited by3

Results whose statement or proof uses this declaration.