Mathlib Map

Theorems · Theorem · field theory

Rat.cast_intCast

∀ {α : Type u_3} [inst : DivisionRing α] (n : ℤ), ↑↑n = ↑n
Defined in
Mathlib.Data.Rat.Cast.Defs
Cited by
74 results in Mathlib
Foundations
Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DivisionRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Rat.cast_natCast · cited by 67Rat.cast_natCastRat.cast_one · cited by 52Rat.cast_oneRat.cast_zero · cited by 29Rat.cast_zeroexists_rat_btwn · cited by 26exists_rat_btwnexists_rat_lt · cited by 5exists_rat_ltPadic.norm_intCast_lt_one_iff · cited by 3Padic.norm_intCast_lt_one…isCusp_SL2Z_iff · cited by 3isCusp_SL2Z_iffRat.cast_divInt · cited by 3Rat.cast_divIntReal.exists_isLUB · cited by 3Real.exists_isLUBIrrational.intCast_add · cited by 3Irrational.intCast_addIrrational.ne_int · cited by 3Irrational.ne_intPadicInt.isUnit_den · cited by 3PadicInt.isUnit_denIrrational.of_intCast_add · cited by 3Irrational.of_intCast_addReal.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational · cited by 2Real.infinite_rat_abs_sub…Irrational.sub_intCast · cited by 2Irrational.sub_intCastNat.cast_one · cited by 2501Nat.cast_oneDivisionRing · cited by 1062DivisionRingdiv_one · cited by 629div_oneRat.cast_def · cited by 20Rat.cast_defRat.cast_intCastCITED BYCITES

Cites4

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

Cited by74

Results whose statement or proof uses this declaration.