Theorems · Theorem · number theory
LiouvilleWith.ne_cast_int
∀ {p x : ℝ}, LiouvilleWith p x → 1 < p → ∀ (m : ℤ), x ≠ ↑m- Cited by
- 1 results in Mathlib
- Foundations
- Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Nat.cast_oneproof · cited by 2,501
- zero_addproof · cited by 2,366
- absproof · cited by 1,814
- LT.lt.ne'proof · cited by 1,417
- le_of_ltproof · cited by 1,175
- one_divproof · cited by 624
- Int.cast_natCastproof · cited by 393
- Int.cast_oneproof · cited by 371
- LT.lt.not_geproof · cited by 305
- Nat.cast_pos'proof · cited by 219
- sub_ne_zeroproof · cited by 119
Cited by1
Results whose statement or proof uses this declaration.
- LiouvilleWith.irrationalproof · cited by 0