Loogle!

Result

Found 9182 declarations mentioning Field. Of these, only the first 200 are shown.

Field 📋 Mathlib.Algebra.Field.Defs
(K : Type u) : Type u
Field.toCommRing 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : CommRing K
Field.toDiv 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : Div K
Field.toDivisionRing 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : DivisionRing K
Field.toInv 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : Inv K
Field.toNNRatCast 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : NNRatCast K
Field.toNontrivial 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : Nontrivial K
Field.toRatCast 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : RatCast K
Field.toSemifield 📋 Mathlib.Algebra.Field.Defs
{K : Type u_1} [Field K] : Semifield K
Field.toZPow 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : ZPow K
Field.nnqsmul 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : ℚ≥0 → K → K
Field.qsmul 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : ℚ → K → K
Field.nnqsmul_def 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (q : ℚ≥0) (a : K) : Field.nnqsmul q a = ↑q * a
Field.qsmul_def 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (a : ℚ) (x : K) : Field.qsmul a x = ↑a * x
Field.zpow_zero' 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (a : K) : a ^ 0 = 1
Field.div_eq_mul_inv 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (a b : K) : a / b = a * b⁻¹
Field.ratCast_def 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (q : ℚ) : ↑q = ↑q.num / ↑q.den
Field.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (n : ℕ) (a : K) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
Field.inv_zero 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : 0⁻¹ = 0
Field.nnratCast_def 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
Field.zpow_succ' 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (n : ℕ) (a : K) : a ^ ↑n.succ = a ^ ↑n * a
Field.mul_inv_cancel 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (a : K) : a ≠ 0 → a * a⁻¹ = 1
Field.mk 📋 Mathlib.Algebra.Field.Defs
{K : Type u} [toCommRing : CommRing K] [toInv : Inv K] [toDiv : Div K] [toZPow : ZPow K] (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹ := by intros; rfl) (zpow_zero' : ∀ (a : K), a ^ 0 = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial K] [toNNRatCast : NNRatCast K] [toRatCast : RatCast K] (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) (inv_zero : 0⁻¹ = 0) (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den := by intros; rfl) (nnqsmul : ℚ≥0 → K → K) (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a := by intros; rfl) (ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den := by intros; rfl) (qsmul : ℚ → K → K) (qsmul_def : ∀ (a : ℚ) (x : K), qsmul a x = ↑a * x := by intros; rfl) : Field K
Field.toGrindField 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] : Lean.Grind.Field K
Lex.instField 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] : Field (Lex K)
OrderDual.instField 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] : Field Kᵒᵈ
Field.isDomain 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] : IsDomain K
Field.ofIsUnitOrEqZero 📋 Mathlib.Algebra.Field.Basic
{R : Type u_3} [Nontrivial R] [CommRing R] (h : ∀ (a : R), IsUnit a ∨ a = 0) : Field R
div_sub' 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] {a b c : K} (hc : c ≠ 0) : a / c - b = (a - c * b) / c
sub_div' 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] {a b c : K} (hc : c ≠ 0) : b - a / c = (b * c - a) / c
inv_sub_inv 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b)
div_sub_div 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} [Field K] (a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)
Function.Injective.field 📋 Mathlib.Algebra.Field.Basic
{K : Type u_1} {L : Type u_2} [Zero K] [Add K] [Neg K] [Sub K] [One K] [Mul K] [Inv K] [Div K] [SMul ℕ K] [SMul ℤ K] [SMul ℚ≥0 K] [SMul ℚ K] [Pow K ℕ] [Pow K ℤ] [NatCast K] [IntCast K] [NNRatCast K] [RatCast K] (f : K → L) (hf : Function.Injective f) [Field L] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : K), f (x + y) = f x + f y) (mul : ∀ (x y : K), f (x * y) = f x * f y) (neg : ∀ (x : K), f (-x) = -f x) (sub : ∀ (x y : K), f (x - y) = f x - f y) (inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : K), f (x / y) = f x / f y) (nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x) (npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) (nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q) (ratCast : ∀ (q : ℚ), f ↑q = ↑q) : Field K
inv_antitoneOn_Iio 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : AntitoneOn (fun x => x⁻¹) (Set.Iio 0)
inv_antitoneOn_Ioi 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
abs_inv 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : |a⁻¹| = |a|⁻¹
sub_inv_antitoneOn_Iio 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun x => (x - c)⁻¹) (Set.Iio c)
sub_inv_antitoneOn_Ioi 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
inv_antitoneOn_Icc_left 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
inv_antitoneOn_Icc_right 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) : AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
abs_div 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) : |a / b| = |a| / |b|
exists_add_lt_and_pos_of_lt 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (h : b < a) : ∃ c, b + c < a ∧ 0 < c
inv_lt_zero' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} : a⁻¹ < 0 ↔ a < 0
inv_nonpos' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0
sub_inv_antitoneOn_Icc_left 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (ha : b < c) : AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
sub_inv_antitoneOn_Icc_right 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (ha : c < a) : AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
le_of_forall_sub_le 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a
div_le_div_of_nonpos_of_le 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c
div_le_one_of_ge 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1
div_lt_div_of_neg_of_lt 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) (h : b < a) : a / c < b / c
div_le_div_right_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a / c ≤ b / c ↔ b ≤ a
div_le_one_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : a / b ≤ 1 ↔ b ≤ a
div_lt_div_right_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a / c < b / c ↔ b < a
div_lt_one_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : a / b < 1 ↔ b < a
one_le_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : 1 ≤ a / b ↔ a ≤ b
one_lt_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : 1 < a / b ↔ a < b
abs_one_div 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : |1 / a| = 1 / |a|
div_le_iff_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b
div_le_iff_of_neg' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b
div_lt_iff_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c < a ↔ a * c < b
div_lt_iff_of_neg' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c < a ↔ c * a < b
le_div_iff_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c
le_div_iff_of_neg' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a
lt_div_iff_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a < b / c ↔ b < a * c
lt_div_iff_of_neg' 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a < b / c ↔ b < c * a
sub_self_div_two 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] (a : α) : a - a / 2 = a / 2
max_div_div_right_of_nonpos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : c ≤ 0) (a b : α) : max (a / c) (b / c) = min a b / c
min_div_div_right_of_nonpos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : c ≤ 0) (a b : α) : min (a / c) (b / c) = max a b / c
div_neg_of_neg_of_pos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : 0 < b) : a / b < 0
div_neg_of_pos_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : b < 0) : a / b < 0
div_nonneg_of_nonpos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a / b
div_pos_of_neg_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a / b
le_mul_of_forall_lt₀ 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b
add_sub_div_two_lt 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (h : a < b) : a + (b - a) / 2 < b
div_two_sub_self 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] (a : α) : a / 2 - a = -(a / 2)
le_of_neg_of_one_div_le_one_div 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) (h : 1 / a ≤ 1 / b) : b ≤ a
lt_of_neg_of_one_div_lt_one_div 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) (h : 1 / a < 1 / b) : b < a
one_div_le_one_div_of_neg_of_le 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a
one_div_lt_one_div_of_neg_of_lt 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) (h : a < b) : 1 / b < 1 / a
inv_le_inv_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a
inv_le_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a
inv_lt_inv_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ < b⁻¹ ↔ b < a
inv_lt_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ < b ↔ b⁻¹ < a
le_inv_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a ≤ b⁻¹ ↔ b ≤ a⁻¹
lt_inv_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹
le_one_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a
lt_one_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a
one_div_le_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a ≤ b ↔ 1 / b ≤ a
one_div_le_one_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a ≤ 1 / b ↔ b ≤ a
one_div_lt_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a < b ↔ 1 / b < a
one_div_lt_one_div_of_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a < 1 / b ↔ b < a
one_le_div_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
one_lt_div_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
one_div_le_neg_one 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1
one_div_lt_neg_one 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1
div_le_one_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
div_lt_one_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
sub_one_div_inv_le_two 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2
div_neg_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
div_nonneg_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
div_nonpos_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
div_pos_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
div_le_div_of_mul_sub_mul_div_nonpos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) ≤ 0 → a / c ≤ b / d
div_lt_div_of_mul_sub_mul_div_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) < 0 → a / c < b / d
mul_sub_mul_div_mul_neg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : a / c < b / d → (a * d - b * c) / (c * d) < 0
mul_sub_mul_div_mul_nonpos 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : a / c ≤ b / d → (a * d - b * c) / (c * d) ≤ 0
mul_sub_mul_div_mul_neg_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
mul_sub_mul_div_mul_nonpos_iff 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [PartialOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
mul_le_of_forall_lt_of_nonneg 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c
two_mul_le_add_mul_sq 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ε : α} (hε : 0 < ε) : 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2
uniform_continuous_npow_on_bounded 📋 Mathlib.Algebra.Order.Field.Basic
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) : ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Rat.instField 📋 Mathlib.Algebra.Field.Rat
: Field ℚ
Mathlib.Tactic.CancelDenoms.cancel_factors_eq_div 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] {n e e' : α} (h : n * e = e') (h2 : n ≠ 0) : e = e' / n
Mathlib.Tactic.CancelDenoms.inv_subst 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] {n k e : α} (h2 : e ≠ 0) (h3 : n * e = k) : k * e⁻¹ = n
Mathlib.Tactic.CancelDenoms.div_subst 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] {n1 n2 k e1 e2 t1 : α} (h1 : n1 * e1 = t1) (h2 : n2 / e2 = 1) (h3 : n1 * n2 = k) : k * (e1 / e2) = t1
Mathlib.Tactic.CancelDenoms.cancel_factors_eq 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))
Mathlib.Tactic.CancelDenoms.cancel_factors_ne 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
Mathlib.Tactic.CancelDenoms.cancel_factors_le 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) : (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
Mathlib.Tactic.CancelDenoms.cancel_factors_lt 📋 Mathlib.Tactic.CancelDenoms.Core
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) : (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
Nonneg.linearOrderedCommGroupWithZero 📋 Mathlib.Algebra.Order.Nonneg.Field
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] : LinearOrderedCommGroupWithZero (Nonneg α)
Rat.castOrderEmbedding 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : ℚ ↪o K
Rat.cast_mono 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Monotone Rat.cast
Rat.cast_strictMono 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : StrictMono Rat.cast
Rat.cast_abs 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) : ↑|q| = |↑q|
Rat.cast_le 📋 Mathlib.Data.Rat.Cast.Order
{p q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : ↑p ≤ ↑q ↔ p ≤ q
Rat.cast_lt 📋 Mathlib.Data.Rat.Cast.Order
{p q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : ↑p < ↑q ↔ p < q
Rat.preimage_cast_Ici 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) : Rat.cast ⁻¹' Set.Ici ↑q = Set.Ici q
Rat.preimage_cast_Iic 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) : Rat.cast ⁻¹' Set.Iic ↑q = Set.Iic q
Rat.preimage_cast_Iio 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) : Rat.cast ⁻¹' Set.Iio ↑q = Set.Iio q
Rat.preimage_cast_Ioi 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) : Rat.cast ⁻¹' Set.Ioi ↑q = Set.Ioi q
Rat.preimage_cast_uIoc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q
Rat.cast_max 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : ↑(max p q) = max ↑p ↑q
Rat.cast_min 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : ↑(min p q) = min ↑p ↑q
Rat.preimage_cast_uIcc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
Rat.cast_le_intCast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ} : ↑m ≤ ↑n ↔ m ≤ ↑n
Rat.cast_lt_intCast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ} : ↑m < ↑n ↔ m < ↑n
Rat.intCast_le_cast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ} : ↑m ≤ ↑n ↔ ↑m ≤ n
Rat.intCast_lt_cast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ} : ↑m < ↑n ↔ ↑m < n
Rat.cast_le_natCast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ} : ↑m ≤ ↑n ↔ m ≤ ↑n
Rat.cast_lt_natCast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ} : ↑m < ↑n ↔ m < ↑n
Rat.natCast_le_cast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ} : ↑m ≤ ↑n ↔ ↑m ≤ n
Rat.natCast_lt_cast 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ} : ↑m < ↑n ↔ ↑m < n
Rat.cast_pos_of_pos 📋 Mathlib.Data.Rat.Cast.Order
{q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (hq : 0 < q) : 0 < ↑q
Rat.preimage_cast_Icc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
Rat.preimage_cast_Ico 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
Rat.preimage_cast_Ioc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
Rat.preimage_cast_Ioo 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
Rat.cast_lt_zero 📋 Mathlib.Data.Rat.Cast.Order
{q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : ↑q < 0 ↔ q < 0
Rat.cast_nonneg 📋 Mathlib.Data.Rat.Cast.Order
{q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : 0 ≤ ↑q ↔ 0 ≤ q
Rat.cast_nonpos 📋 Mathlib.Data.Rat.Cast.Order
{q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : ↑q ≤ 0 ↔ q ≤ 0
Rat.cast_pos 📋 Mathlib.Data.Rat.Cast.Order
{q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : 0 < ↑q ↔ 0 < q
Rat.castOrderEmbedding_apply 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (a✝ : ℚ) : Rat.castOrderEmbedding a✝ = ↑a✝
Int.floor_div_natCast 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] (a : k) (n : ℕ) : ⌊a / ↑n⌋ = ⌊a⌋ / ↑n
Int.floor_div_cast_of_nonneg 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / ↑n⌋ = ⌊a⌋ / n
Int.fract_div_intCast_eq_div_intCast_mod 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {m : ℤ} {n : ℕ} : Int.fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
Int.fract_div_natCast_eq_div_natCast_mod 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {m n : ℕ} : Int.fract (↑m / ↑n) = ↑(m % n) / ↑n
Int.div_two_lt_floor 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) : a / 2 < ↑⌊a⌋
Int.fract_div_mul_self_add_zsmul_eq 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [FloorRing k] (a b : k) (ha : a ≠ 0) : Int.fract (b / a) * a + ⌊b / a⌋ • a = b
Int.fract_div_mul_self_mem_Ico 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] (a b : k) (ha : 0 < a) : Int.fract (b / a) * a ∈ Set.Ico 0 a
Int.sub_floor_div_mul_lt 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) : a - ↑⌊a / b⌋ * b < b
Int.sub_floor_div_mul_nonneg 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) : 0 ≤ a - ↑⌊a / b⌋ * b
Int.ceil_le_two_mul 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ ≤ a) : ↑⌈a⌉ ≤ 2 * a
Int.ceil_lt_two_mul 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ < a) : ↑⌈a⌉ < 2 * a
Int.ceil_le_mul 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a) : ↑⌈a⌉ ≤ b * a
Int.ceil_lt_mul 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b < a) : ↑⌈a⌉ < b * a
Int.ceil_div_ceil_inv_sub_one 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) : ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉
Int.mul_lt_floor 📋 Mathlib.Algebra.Order.Floor.Ring
{k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉ ≤ a) : b * a < ↑⌊a⌋
round_two_inv 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : round 2⁻¹ = 1
round_neg_two_inv 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : round (-2⁻¹) = 0
round_eq 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : round x = ⌊x + 1 / 2⌋
round_le_add_half 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : ↑(round x) ≤ x + 1 / 2
sub_half_lt_round 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : x - 1 / 2 < ↑(round x)
Int.map_round 📋 Mathlib.Algebra.Order.Round
{F : Type u_1} {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : round (f a) = round a
abs_sub_round 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : |x - ↑(round x)| ≤ 1 / 2
round_eq_zero_iff 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} : round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)
abs_sub_round_div_natCast_eq 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {m n : ℕ} : |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
round_eq_iff 📋 Mathlib.Algebra.Order.Round
{α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} {n : ℤ} : round x = n ↔ x ∈ Set.Ico (↑n - 1 / 2) (↑n + 1 / 2)
Rat.ceil_cast 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) : ⌈↑x⌉ = ⌈x⌉
Rat.floor_cast 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) : ⌊↑x⌋ = ⌊x⌋
Rat.round_cast 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) : round ↑x = round x
Rat.cast_fract 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) : ↑(Int.fract x) = Int.fract ↑x
Rat.isInt_intCeil_ofIsRat_neg 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌈r⌉ (Int.negOfNat (n / d))
Rat.isNat_intFloor_ofIsNNRat 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌊r⌋ (n / d)
Rat.isNNRat_intFract_of_isNNRat 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNNRat (Int.fract r) (n % d) d
Rat.isInt_intFloor_ofIsRat_neg 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌊r⌋ (Int.negOfNat (-(-↑n / ↑d)).toNat)
Rat.isRat_intFract_of_isRat_negOfNat 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsRat (Int.fract r) (-↑n % ↑d) d
Rat.IsRat.isInt_round 📋 Mathlib.Data.Rat.Floor
{R : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (n : ℤ) (d : ℕ) (res : ℤ) (hres : round (↑n / ↑d) = res) : Mathlib.Meta.NormNum.IsRat r n d → Mathlib.Meta.NormNum.IsInt (round r) res
Rat.isNat_intCeil_ofIsNNRat 📋 Mathlib.Data.Rat.Floor
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) : Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌈r⌉ (-(-↑n / ↑d)).toNat
NNRat.Nonneg.coe_ofScientific 📋 Mathlib.Data.Rat.Cast.Lemmas
{K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (m : ℕ) (s : Bool) (e : ℕ) : ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
FloorRing.archimedean 📋 Mathlib.Algebra.Order.Archimedean.Basic
(K : Type u_5) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] : Archimedean K
exists_rat_gt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K) : ∃ q, x < ↑q
exists_rat_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K) : ∃ q, ↑q < x
exists_rat_mem_uIoo 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : x ≠ y) : ∃ q, ↑q ∈ Set.uIoo x y
archimedean_iff_rat_le 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ q, x ≤ ↑q
archimedean_iff_rat_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ q, x < ↑q
archimedean_iff_int_le 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ n, x ≤ ↑n
archimedean_iff_int_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ n, x < ↑n
archimedean_iff_nat_le 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ n, x ≤ ↑n
archimedean_iff_nat_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Archimedean K ↔ ∀ (x : K), ∃ n, x < ↑n
eq_of_forall_lt_rat_iff_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
{K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q) : x = y

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c