Theorems · Theorem · field theory
Rat.cast_one
∀ {α : Type u_3} [inst : DivisionRing α], ↑1 = 1- Defined in
- Mathlib.Data.Rat.Cast.Defs
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DivisionRingstatement and proof · cited by 1,062
- Int.cast_oneproof · cited by 371
- Rat.cast_intCastproof · cited by 74
Cited by53
Results whose statement or proof uses this declaration.
- Rat.castHomproof · cited by 33
- Real.zero_lt_oneproof · cited by 5
- NumberField.mixedEmbedding.norm_unitproof · cited by 3
- Real.strictMono_eulerMascheroniSeqproof · cited by 3
- Padic.norm_intCast_lt_one_iffproof · cited by 3
- Real.ofDigits_le_oneproof · cited by 3
- Irrational.mul_ratCastproof · cited by 3
- AntitoneOn.integral_le_sumproof · cited by 3
- LiouvilleWith.mul_rat_iffproof · cited by 3
- bernoulliFun_eval_oneproof · cited by 3
- AntitoneOn.sum_le_integralproof · cited by 2
- Real.strictAnti_eulerMascheroniSeq'proof · cited by 2