Loogle!
Result
Found 1846 declarations mentioning Rat. Of these, only the first 200 are shown.
- Rat π Batteries.Data.Rat.Basic
: Type - instDecidableEqRat π Batteries.Data.Rat.Basic
: DecidableEq β - instInhabitedRat π Batteries.Data.Rat.Basic
: Inhabited β - instReprRat π Batteries.Data.Rat.Basic
: Repr β - instToStringRat π Batteries.Data.Rat.Basic
: ToString β - Rat.ceil π Batteries.Data.Rat.Basic
(a : β) : β€ - Rat.den π Batteries.Data.Rat.Basic
(self : β) : β - Rat.floor π Batteries.Data.Rat.Basic
(a : β) : β€ - Rat.instAdd π Batteries.Data.Rat.Basic
: Add β - Rat.instDiv π Batteries.Data.Rat.Basic
: Div β - Rat.instIntCast π Batteries.Data.Rat.Basic
: IntCast β - Rat.instLE π Batteries.Data.Rat.Basic
: LE β - Rat.instLT π Batteries.Data.Rat.Basic
: LT β - Rat.instMul π Batteries.Data.Rat.Basic
: Mul β - Rat.instNatCast π Batteries.Data.Rat.Basic
: NatCast β - Rat.instNeg π Batteries.Data.Rat.Basic
: Neg β - Rat.instOfScientific π Batteries.Data.Rat.Basic
: OfScientific β - Rat.instSub π Batteries.Data.Rat.Basic
: Sub β - Rat.inv π Batteries.Data.Rat.Basic
(a : β) : β - Rat.isInt π Batteries.Data.Rat.Basic
(a : β) : Bool - Rat.neg π Batteries.Data.Rat.Basic
(a : β) : β - Rat.num π Batteries.Data.Rat.Basic
(self : β) : β€ - Rat.ofInt π Batteries.Data.Rat.Basic
(num : β€) : β - mkRat π Batteries.Data.Rat.Basic
(num : β€) (den : β) : β - Rat.add π Batteries.Data.Rat.Basic
(a b : β) : β - Rat.blt π Batteries.Data.Rat.Basic
(a b : β) : Bool - Rat.div π Batteries.Data.Rat.Basic
: β β β β β - Rat.divInt π Batteries.Data.Rat.Basic
: β€ β β€ β β - Rat.mul π Batteries.Data.Rat.Basic
(a b : β) : β - Rat.sub π Batteries.Data.Rat.Basic
(a b : β) : β - Rat.instOfNat π Batteries.Data.Rat.Basic
{n : β} : OfNat β n - Rat.ofScientific π Batteries.Data.Rat.Basic
(m : β) (s : Bool) (e : β) : β - Rat.reduced π Batteries.Data.Rat.Basic
(self : β) : self.num.natAbs.Coprime self.den - Rat.instDecidableLe π Batteries.Data.Rat.Basic
(a b : β) : Decidable (a β€ b) - Rat.instDecidableLt π Batteries.Data.Rat.Basic
(a b : β) : Decidable (a < b) - Rat.noConfusionType.withCtor π Batteries.Data.Rat.Basic
(P : Type u) (ctorIdx : β) (k : Rat.noConfusionType.withCtorType P ctorIdx) (k' : P) (x : β) : P - Rat.den_nz π Batteries.Data.Rat.Basic
(self : β) : self.den β 0 - Rat.den_pos π Batteries.Data.Rat.Basic
(self : β) : 0 < self.den - Rat.mk' π Batteries.Data.Rat.Basic
(num : β€) (den : β) (den_nz : den β 0 := by decide) (reduced : num.natAbs.Coprime den := by decide) : β - Rat.normalize π Batteries.Data.Rat.Basic
(num : β€) (den : β := 1) (den_nz : den β 0 := by decide) : β - Rat.maybeNormalize π Batteries.Data.Rat.Basic
(num : β€) (den g : β) (dvd_num : βg β£ num) (dvd_den : g β£ den) (den_nz : den / g β 0) (reduced : (num / βg).natAbs.Coprime (den / g)) : β - Rat.mk'.injEq π Batteries.Data.Rat.Basic
(num : β€) (den : β) (den_nz : den β 0 := by decide) (reduced : num.natAbs.Coprime den := by decide) (numβ : β€) (denβ : β) (den_nzβ : denβ β 0 := by decide) (reducedβ : numβ.natAbs.Coprime denβ := by decide) : ({ num := num, den := den, den_nz := den_nz, reduced := reduced } = { num := numβ, den := denβ, den_nz := den_nzβ, reduced := reducedβ }) = (num = numβ β§ den = denβ) - Rat.mk'.sizeOf_spec π Batteries.Data.Rat.Basic
(num : β€) (den : β) (den_nz : den β 0 := by decide) (reduced : num.natAbs.Coprime den := by decide) : sizeOf { num := num, den := den, den_nz := den_nz, reduced := reduced } = 1 + sizeOf num + sizeOf den + sizeOf reduced - Rat.add.aux π Batteries.Data.Rat.Basic
(a b : β) {g ad bd : β} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) : let den := ad * b.den; let num := a.num * βbd + b.num * βad; num.natAbs.gcd g = num.natAbs.gcd den - Rat.sub.aux π Batteries.Data.Rat.Basic
(a b : β) {g ad bd : β} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) : let den := ad * b.den; let num := a.num * βbd - b.num * βad; num.natAbs.gcd g = num.natAbs.gcd den - instRatCastRat π Batteries.Classes.RatCast
: RatCast β - Rat.cast π Batteries.Classes.RatCast
{K : Type u} [RatCast K] : β β K - RatCast.mk π Batteries.Classes.RatCast
{K : Type u} (ratCast : β β K) : RatCast K - RatCast.ratCast π Batteries.Classes.RatCast
{K : Type u} [self : RatCast K] : β β K - instCoeHTCTRatOfRatCast π Batteries.Classes.RatCast
{K : Type u_1} [RatCast K] : CoeHTCT β K - instCoeTailRatOfRatCast π Batteries.Classes.RatCast
{K : Type u_1} [RatCast K] : CoeTail β K - Float.toRat0 π Batteries.Data.Rat.Float
(a : Float) : β - Rat.toFloat π Batteries.Data.Rat.Float
(a : β) : Float - Float.toRat? π Batteries.Data.Rat.Float
(a : Float) : Option β - Rat.instCoeFloat π Batteries.Data.Rat.Float
: Coe β Float - Rat.intCast_num π Batteries.Data.Rat.Lemmas
(a : β€) : (βa).num = a - Rat.mkRat_self π Batteries.Data.Rat.Lemmas
(a : β) : mkRat a.num a.den = a - Rat.neg_den π Batteries.Data.Rat.Lemmas
(a : β) : (-a).den = a.den - Rat.inv_divInt π Batteries.Data.Rat.Lemmas
(n d : β€) : (Rat.divInt n d).inv = Rat.divInt d n - Rat.normalize_self π Batteries.Data.Rat.Lemmas
(r : β) : Rat.normalize r.num r.den β― = r - Rat.divInt_self π Batteries.Data.Rat.Lemmas
(a : β) : Rat.divInt a.num βa.den = a - Rat.divInt_ofNat π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) : Rat.divInt num βden = mkRat num den - Rat.intCast_den π Batteries.Data.Rat.Lemmas
(a : β€) : (βa).den = 1 - Rat.inv_def π Batteries.Data.Rat.Lemmas
(a : β) : a.inv = Rat.divInt (βa.den) a.num - Rat.inv_zero π Batteries.Data.Rat.Lemmas
: Rat.inv 0 = 0 - Rat.neg_num π Batteries.Data.Rat.Lemmas
(a : β) : (-a).num = -a.num - Rat.one_den π Batteries.Data.Rat.Lemmas
: Rat.den 1 = 1 - Rat.one_num π Batteries.Data.Rat.Lemmas
: Rat.num 1 = 1 - Rat.zero_den π Batteries.Data.Rat.Lemmas
: Rat.den 0 = 1 - Rat.zero_num π Batteries.Data.Rat.Lemmas
: Rat.num 0 = 0 - Rat.divInt.eq_1 π Batteries.Data.Rat.Lemmas
(xβ : β€) (d : β) : Rat.divInt xβ (Int.ofNat d) = inline (mkRat xβ d) - Rat.ofInt_ofNat π Batteries.Data.Rat.Lemmas
{n : β} : Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n - Rat.ofNat_den π Batteries.Data.Rat.Lemmas
{n : β} : Rat.den (OfNat.ofNat n) = 1 - Rat.ofNat_num π Batteries.Data.Rat.Lemmas
{n : β} : Rat.num (OfNat.ofNat n) = OfNat.ofNat n - Rat.divInt_zero π Batteries.Data.Rat.Lemmas
(n : β€) : Rat.divInt n 0 = 0 - Rat.intCast_one π Batteries.Data.Rat.Lemmas
: β1 = 1 - Rat.intCast_zero π Batteries.Data.Rat.Lemmas
: β0 = 0 - Rat.mkRat_zero π Batteries.Data.Rat.Lemmas
(n : β€) : mkRat n 0 = 0 - Rat.zero_divInt π Batteries.Data.Rat.Lemmas
(n : β€) : Rat.divInt 0 n = 0 - Rat.zero_mkRat π Batteries.Data.Rat.Lemmas
(n : β) : mkRat 0 n = 0 - Rat.divInt_neg' π Batteries.Data.Rat.Lemmas
(num den : β€) : Rat.divInt num (-den) = Rat.divInt (-num) den - Rat.neg_divInt π Batteries.Data.Rat.Lemmas
(n d : β€) : -Rat.divInt n d = Rat.divInt (-n) d - Rat.neg_divInt_neg π Batteries.Data.Rat.Lemmas
(num den : β€) : Rat.divInt (-num) (-den) = Rat.divInt num den - Rat.neg_mkRat π Batteries.Data.Rat.Lemmas
(n : β€) (d : β) : -mkRat n d = mkRat (-n) d - Rat.intCast_inj π Batteries.Data.Rat.Lemmas
{a b : β€} : βa = βb β a = b - Rat.intCast_neg π Batteries.Data.Rat.Lemmas
(a : β€) : β(-a) = -βa - Rat.mul_one π Batteries.Data.Rat.Lemmas
(a : β) : a * 1 = a - Rat.one_mul π Batteries.Data.Rat.Lemmas
(a : β) : 1 * a = a - Rat.divInt.eq_2 π Batteries.Data.Rat.Lemmas
(xβ : β€) (d : β) : Rat.divInt xβ (Int.negSucc d) = Rat.normalize (-xβ) d.succ β― - Rat.ext π Batteries.Data.Rat.Lemmas
{p q : β} : p.num = q.num β p.den = q.den β p = q - Rat.mk_den_one π Batteries.Data.Rat.Lemmas
{r : β€} : { num := r, den_nz := Nat.one_ne_zero, reduced := β― } = βr - Rat.mul_zero π Batteries.Data.Rat.Lemmas
(a : β) : a * 0 = 0 - Rat.zero_mul π Batteries.Data.Rat.Lemmas
(a : β) : 0 * a = 0 - Rat.mul_comm π Batteries.Data.Rat.Lemmas
(a b : β) : a * b = b * a - Rat.div_def π Batteries.Data.Rat.Lemmas
(a b : β) : a / b = a * b.inv - Rat.mk_eq_mkRat π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) (nz : den β 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = mkRat num den - Rat.ofScientific_ofNat_ofNat π Batteries.Data.Rat.Lemmas
{m : β} {s : Bool} {e : β} : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e - Rat.sub_eq_add_neg π Batteries.Data.Rat.Lemmas
(a b : β) : a - b = a + -b - Rat.mk_eq_divInt π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) (nz : den β 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num βden - Rat.mkRat_eq_zero π Batteries.Data.Rat.Lemmas
{d : β} {n : β€} (d0 : d β 0) : mkRat n d = 0 β n = 0 - Rat.mkRat_ne_zero π Batteries.Data.Rat.Lemmas
{d : β} {n : β€} (d0 : d β 0) : mkRat n d β 0 β n β 0 - Rat.ofScientific_true_def π Batteries.Data.Rat.Lemmas
{m e : β} : Rat.ofScientific m true e = mkRat (βm) (10 ^ e) - Rat.normalize_eq_zero π Batteries.Data.Rat.Lemmas
{d : β} {n : β€} (d0 : d β 0) : Rat.normalize n d d0 = 0 β n = 0 - Rat.intCast_add π Batteries.Data.Rat.Lemmas
(a b : β€) : β(a + b) = βa + βb - Rat.intCast_mul π Batteries.Data.Rat.Lemmas
(a b : β€) : β(a * b) = βa * βb - Rat.intCast_sub π Batteries.Data.Rat.Lemmas
(a b : β€) : β(a - b) = βa - βb - Rat.normalize_eq_mkRat π Batteries.Data.Rat.Lemmas
{num : β€} {den : β} (den_nz : den β 0) : Rat.normalize num den den_nz = mkRat num den - Rat.divInt_mul_left π Batteries.Data.Rat.Lemmas
{n d a : β€} (a0 : a β 0) : Rat.divInt (a * n) (a * d) = Rat.divInt n d - Rat.divInt_mul_right π Batteries.Data.Rat.Lemmas
{n d a : β€} (a0 : a β 0) : Rat.divInt (n * a) (d * a) = Rat.divInt n d - Rat.ofScientific_false_def π Batteries.Data.Rat.Lemmas
{m e : β} : Rat.ofScientific m false e = β(m * 10 ^ e) - Rat.normalize_zero π Batteries.Data.Rat.Lemmas
{d : β} (nz : d β 0) : Rat.normalize 0 d nz = 0 - Rat.mk_eq_normalize π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) (nz : den β 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz - Rat.mkRat_mul_left π Batteries.Data.Rat.Lemmas
{n : β€} {d a : β} (a0 : a β 0) : mkRat (βa * n) (a * d) = mkRat n d - Rat.mkRat_mul_mkRat π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) (dβ dβ : β) : mkRat nβ dβ * mkRat nβ dβ = mkRat (nβ * nβ) (dβ * dβ) - Rat.mkRat_mul_right π Batteries.Data.Rat.Lemmas
{n : β€} {d a : β} (a0 : a β 0) : mkRat (n * βa) (d * a) = mkRat n d - Rat.neg_normalize π Batteries.Data.Rat.Lemmas
(n : β€) (d : β) (z : d β 0) : -Rat.normalize n d z = Rat.normalize (-n) d z - Rat.mul_def π Batteries.Data.Rat.Lemmas
(a b : β) : a * b = Rat.normalize (a.num * b.num) (a.den * b.den) β― - Rat.divInt_eq_iff π Batteries.Data.Rat.Lemmas
{dβ dβ nβ nβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.divInt nβ dβ = Rat.divInt nβ dβ β nβ * dβ = nβ * dβ - Rat.normalize.eq_1 π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) (den_nz : den β 0) : Rat.normalize num den den_nz = Rat.maybeNormalize num den (num.natAbs.gcd den) β― β― β― β― - Rat.mkRat_def π Batteries.Data.Rat.Lemmas
(n : β€) (d : β) : mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0 - Rat.normalize_mul_left π Batteries.Data.Rat.Lemmas
{d : β} {n : β€} {a : β} (d0 : d β 0) (a0 : a β 0) : Rat.normalize (βa * n) (a * d) β― = Rat.normalize n d d0 - Rat.normalize_mul_right π Batteries.Data.Rat.Lemmas
{d : β} {n : β€} {a : β} (d0 : d β 0) (a0 : a β 0) : Rat.normalize (n * βa) (d * a) β― = Rat.normalize n d d0 - Rat.divInt_mul_divInt π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.divInt nβ dβ * Rat.divInt nβ dβ = Rat.divInt (nβ * nβ) (dβ * dβ) - Rat.mkRat_eq_iff π Batteries.Data.Rat.Lemmas
{dβ dβ : β} {nβ nβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : mkRat nβ dβ = mkRat nβ dβ β nβ * βdβ = nβ * βdβ - Rat.normalize_eq_iff π Batteries.Data.Rat.Lemmas
{dβ dβ : β} {nβ nβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.normalize nβ dβ zβ = Rat.normalize nβ dβ zβ β nβ * βdβ = nβ * βdβ - mkRat.eq_1 π Batteries.Data.Rat.Lemmas
(num : β€) (den : β) : mkRat num den = if den_nz : den = 0 then { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 } else Rat.normalize num den den_nz - Rat.add_def' π Batteries.Data.Rat.Lemmas
(a b : β) : a + b = mkRat (a.num * βb.den + b.num * βa.den) (a.den * b.den) - Rat.sub_def' π Batteries.Data.Rat.Lemmas
(a b : β) : a - b = mkRat (a.num * βb.den - b.num * βa.den) (a.den * b.den) - Rat.ofScientific_def π Batteries.Data.Rat.Lemmas
{m : β} {s : Bool} {e : β} : Rat.ofScientific m s e = if s = true then mkRat (βm) (10 ^ e) else β(m * 10 ^ e) - Rat.add_def π Batteries.Data.Rat.Lemmas
(a b : β) : a + b = Rat.normalize (a.num * βb.den + b.num * βa.den) (a.den * b.den) β― - Rat.sub_def π Batteries.Data.Rat.Lemmas
(a b : β) : a - b = Rat.normalize (a.num * βb.den - b.num * βa.den) (a.den * b.den) β― - Rat.divInt_add_divInt π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.divInt nβ dβ + Rat.divInt nβ dβ = Rat.divInt (nβ * dβ + nβ * dβ) (dβ * dβ) - Rat.divInt_sub_divInt π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β€} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.divInt nβ dβ - Rat.divInt nβ dβ = Rat.divInt (nβ * dβ - nβ * dβ) (dβ * dβ) - Rat.divInt_num_den π Batteries.Data.Rat.Lemmas
{d n n' : β€} {d' : β} {z' : d' β 0} {c : n'.natAbs.Coprime d'} (z : d β 0) (h : Rat.divInt n d = { num := n', den := d', den_nz := z', reduced := c }) : β m, m β 0 β§ n = n' * m β§ d = βd' * m - Rat.mkRat_num_den π Batteries.Data.Rat.Lemmas
{d : β} {n n' : β€} {d' : β} {z' : d' β 0} {c : n'.natAbs.Coprime d'} (z : d β 0) (h : mkRat n d = { num := n', den := d', den_nz := z', reduced := c }) : β m, m β 0 β§ n = n' * βm β§ d = d' * m - Rat.mkRat_add_mkRat π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β} (zβ : dβ β 0) (zβ : dβ β 0) : mkRat nβ dβ + mkRat nβ dβ = mkRat (nβ * βdβ + nβ * βdβ) (dβ * dβ) - Rat.normalize_eq π Batteries.Data.Rat.Lemmas
{num : β€} {den : β} (den_nz : den β 0) : Rat.normalize num den den_nz = { num := num / β(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := β―, reduced := β― } - Rat.maybeNormalize_eq π Batteries.Data.Rat.Lemmas
{num : β€} {den g : β} (dvd_num : βg β£ num) (dvd_den : g β£ den) (den_nz : den / g β 0) (reduced : (num / βg).natAbs.Coprime (den / g)) : Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced = { num := num.divExact (βg) dvd_num, den := den / g, den_nz := den_nz, reduced := reduced } - Rat.normalize_mul_normalize π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.normalize nβ dβ zβ * Rat.normalize nβ dβ zβ = Rat.normalize (nβ * nβ) (dβ * dβ) β― - Rat.normalize_num_den π Batteries.Data.Rat.Lemmas
{n : β€} {d : β} {z : d β 0} {n' : β€} {d' : β} {z' : d' β 0} {c : n'.natAbs.Coprime d'} (h : Rat.normalize n d z = { num := n', den := d', den_nz := z', reduced := c }) : β m, m β 0 β§ n = n' * βm β§ d = d' * m - Rat.normalize_add_normalize π Batteries.Data.Rat.Lemmas
(nβ nβ : β€) {dβ dβ : β} (zβ : dβ β 0) (zβ : dβ β 0) : Rat.normalize nβ dβ zβ + Rat.normalize nβ dβ zβ = Rat.normalize (nβ * βdβ + nβ * βdβ) (dβ * dβ) β― - Rat.maybeNormalize_eq_normalize π Batteries.Data.Rat.Lemmas
{num : β€} {den g : β} (dvd_num : βg β£ num) (dvd_den : g β£ den) (den_nz : den / g β 0) (reduced : (num / βg).natAbs.Coprime (den / g)) (hn : βg β£ num) (hd : g β£ den) : Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced = Rat.normalize num den β― - Lean.Expr.rat? π Mathlib.Lean.Expr.Rat
(e : Lean.Expr) : Option β - Rat.instNNRatCast π Mathlib.Data.Rat.Init
: NNRatCast β - Rat.cast_eq_id π Mathlib.Data.Rat.Init
: Rat.cast = id - Rat.cast_id π Mathlib.Data.Rat.Init
(n : β) : βn = n - NNRat.den_mk π Mathlib.Data.Rat.Init
(q : β) (hq : 0 β€ q) : NNRat.den β¨q, hqβ© = q.den - NNRat.num_mk π Mathlib.Data.Rat.Init
(q : β) (hq : 0 β€ q) : NNRat.num β¨q, hqβ© = q.num.natAbs - DivisionRing.qsmul π Mathlib.Algebra.Field.Defs
{K : Type u_2} [self : DivisionRing K] : β β K β K - Field.qsmul π Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] : β β K β K - Rat.smulDivisionRing π Mathlib.Algebra.Field.Defs
{K : Type u_1} [DivisionRing K] : SMul β K - Rat.castRec π Mathlib.Algebra.Field.Defs
{K : Type u_1} [NatCast K] [IntCast K] [Div K] (q : β) : K - Rat.ofScientific_eq_ofScientific π Mathlib.Algebra.Field.Defs
(m : β) (s : Bool) (e : β) : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e - DivisionRing.qsmul_def π Mathlib.Algebra.Field.Defs
{K : Type u_2} [self : DivisionRing K] (a : β) (x : K) : DivisionRing.qsmul a x = βa * x - Rat.smul_one_eq_cast π Mathlib.Algebra.Field.Defs
(A : Type u_2) [DivisionRing A] (m : β) : m β’ 1 = βm - Field.qsmul_def π Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (a : β) (x : K) : Field.qsmul a x = βa * x - DivisionRing.ratCast_def π Mathlib.Algebra.Field.Defs
{K : Type u_2} [self : DivisionRing K] (q : β) : βq = βq.num / βq.den - Field.ratCast_def π Mathlib.Algebra.Field.Defs
{K : Type u} [self : Field K] (q : β) : βq = βq.num / βq.den - Rat.smul_def π Mathlib.Algebra.Field.Defs
{K : Type u_1} [DivisionRing K] (a : β) (x : K) : a β’ x = βa * x - Rat.cast_def π Mathlib.Algebra.Field.Defs
{K : Type u_1} [DivisionRing K] (q : β) : βq = βq.num / βq.den - DivisionRing.mk π Mathlib.Algebra.Field.Defs
{K : Type u_2} [toRing : Ring K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : β (a b : K), a / b = a * bβ»ΒΉ := by intros; rfl) (zpow : β€ β K β K) (zpow_zero' : β (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : β (n : β) (a : K), zpow (βn.succ) a = zpow (βn) a * a := by intros; rfl) (zpow_neg' : β (n : β) (a : K), zpow (Int.negSucc n) a = (zpow (βn.succ) a)β»ΒΉ := 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) : DivisionRing K - Field.mk π Mathlib.Algebra.Field.Defs
{K : Type u} [toCommRing : CommRing K] [toInv : Inv K] [toDiv : Div K] (div_eq_mul_inv : β (a b : K), a / b = a * bβ»ΒΉ := by intros; rfl) (zpow : β€ β K β K) (zpow_zero' : β (a : K), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : β (n : β) (a : K), zpow (βn.succ) a = zpow (βn) a * a := by intros; rfl) (zpow_neg' : β (n : β) (a : K), zpow (Int.negSucc n) a = (zpow (βn.succ) a)β»ΒΉ := 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 - Mathlib.Meta.NormNum.Result'.isRat π Mathlib.Tactic.NormNum.Result
(inst : Lean.Expr) (q : β) (n d proof : Lean.Expr) : Mathlib.Meta.NormNum.Result' - Mathlib.Meta.NormNum.mkRawRatLit π Mathlib.Tactic.NormNum.Result
(q : β) : Q(β) - Mathlib.Meta.NormNum.Result.toRat π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} {e : Q(Β«$Ξ±Β»)} : Mathlib.Meta.NormNum.Result e β Option β - Mathlib.Meta.NormNum.Result.toRatNZ π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} {e : Q(Β«$Ξ±Β»)} : Mathlib.Meta.NormNum.Result e β Option (β Γ Option Lean.Expr) - Mathlib.Meta.NormNum.Result.ofRawRat π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} (q : β) (e : Q(Β«$Ξ±Β»)) (hyp : Option Lean.Expr := none) : Mathlib.Meta.NormNum.Result e - Mathlib.Meta.NormNum.Result'.isRat.injEq π Mathlib.Tactic.NormNum.Result
(inst : Lean.Expr) (q : β) (n d proof instβ : Lean.Expr) (qβ : β) (nβ dβ proofβ : Lean.Expr) : (Mathlib.Meta.NormNum.Result'.isRat inst q n d proof = Mathlib.Meta.NormNum.Result'.isRat instβ qβ nβ dβ proofβ) = (inst = instβ β§ q = qβ β§ n = nβ β§ d = dβ β§ proof = proofβ) - Mathlib.Meta.NormNum.Result.isRat π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} {x : Q(Β«$Ξ±Β»)} (inst : Q(DivisionRing Β«$Ξ±Β») := by assumption) (q : β) (n : Q(β€)) (d : Q(β)) (proof : Q(Mathlib.Meta.NormNum.IsRat Β«$xΒ» Β«$nΒ» Β«$dΒ»)) : Mathlib.Meta.NormNum.Result x - Mathlib.Meta.NormNum.Result.isRat' π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} {x : Q(Β«$Ξ±Β»)} (inst : Q(DivisionRing Β«$Ξ±Β») := by assumption) (q : β) (n : Q(β€)) (d : Q(β)) (proof : Q(Mathlib.Meta.NormNum.IsRat Β«$xΒ» Β«$nΒ» Β«$dΒ»)) : Mathlib.Meta.NormNum.Result x - Mathlib.Meta.NormNum.Result'.isRat.sizeOf_spec π Mathlib.Tactic.NormNum.Result
(inst : Lean.Expr) (q : β) (n d proof : Lean.Expr) : sizeOf (Mathlib.Meta.NormNum.Result'.isRat inst q n d proof) = 1 + sizeOf inst + sizeOf q + sizeOf n + sizeOf d + sizeOf proof - Mathlib.Meta.NormNum.Result.toRat' π Mathlib.Tactic.NormNum.Result
{u : Lean.Level} {Ξ± : Q(Type u)} {e : Q(Β«$Ξ±Β»)} (_i : Q(DivisionRing Β«$Ξ±Β») := by with_reducible assumption) : Mathlib.Meta.NormNum.Result e β Option (β Γ (n : Q(β€)) Γ (d : Q(β)) Γ Q(Mathlib.Meta.NormNum.IsRat Β«$eΒ» Β«$nΒ» Β«$dΒ»)) - Mathlib.Meta.NormNum.deriveRat π Mathlib.Tactic.NormNum.Core
{u : Lean.Level} {Ξ± : Q(Type u)} (e : Q(Β«$Ξ±Β»)) (_inst : Q(DivisionRing Β«$Ξ±Β») := by with_reducible assumption) : Lean.MetaM (β Γ (n : Q(β€)) Γ (d : Q(β)) Γ Q(Mathlib.Meta.NormNum.IsRat Β«$eΒ» Β«$nΒ» Β«$dΒ»)) - ofDual_ratCast π Mathlib.Algebra.Field.Basic
{K : Type u_1} [RatCast K] (n : β) : OrderDual.ofDual βn = βn - ofLex_ratCast π Mathlib.Algebra.Field.Basic
{K : Type u_1} [RatCast K] (n : β) : ofLex βn = βn - toDual_ratCast π Mathlib.Algebra.Field.Basic
{K : Type u_1} [RatCast K] (n : β) : OrderDual.toDual βn = βn - toLex_ratCast π Mathlib.Algebra.Field.Basic
{K : Type u_1} [RatCast K] (n : β) : toLex βn = βn - Function.Injective.divisionRing π 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) [DivisionRing 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) : DivisionRing K - 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 - Linarith.SimplexAlgorithm.DenseMatrix.data π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (self : Linarith.SimplexAlgorithm.DenseMatrix n m) : Array (Array β) - Linarith.SimplexAlgorithm.DenseMatrix.mk π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data : Array (Array β)) : Linarith.SimplexAlgorithm.DenseMatrix n m - Linarith.SimplexAlgorithm.SparseMatrix.data π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (self : Linarith.SimplexAlgorithm.SparseMatrix n m) : Array (Std.HashMap β β) - Linarith.SimplexAlgorithm.SparseMatrix.mk π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data : Array (Std.HashMap β β)) : Linarith.SimplexAlgorithm.SparseMatrix n m - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.getElem π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (mat : Ξ± n m) (i j : β) : β - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.divideRow π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (mat : Ξ± n m) (i : β) (coef : β) : Ξ± n m - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.getValues π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (mat : Ξ± n m) : List (β Γ β Γ β) - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.ofValues π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (values : List (β Γ β Γ β)) : Ξ± n m - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.setElem π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (mat : Ξ± n m) (i j : β) (v : β) : Ξ± n m - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.subtractRow π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} [self : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ±] {n m : β} (mat : Ξ± n m) (i j : β) (coef : β) : Ξ± n m - Linarith.SimplexAlgorithm.DenseMatrix.mk.injEq π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data dataβ : Array (Array β)) : ({ data := data } = { data := dataβ }) = (data = dataβ) - Linarith.SimplexAlgorithm.instGetElemProdNatRatAndLtFstSndOfUsableInSimplexAlgorithm π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
(n m : β) (matType : β β β β Type) [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] : GetElem (matType n m) (β Γ β) β fun x p => p.1 < n β§ p.2 < m - Linarith.SimplexAlgorithm.DenseMatrix.mk.sizeOf_spec π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data : Array (Array β)) : sizeOf { data := data } = 1 + sizeOf data - Linarith.SimplexAlgorithm.SparseMatrix.mk.injEq π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data dataβ : Array (Std.HashMap β β)) : ({ data := data } = { data := dataβ }) = (data = dataβ) - Linarith.SimplexAlgorithm.SparseMatrix.mk.sizeOf_spec π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{n m : β} (data : Array (Std.HashMap β β)) : sizeOf { data := data } = 1 + sizeOf data - Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.mk π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
{Ξ± : β β β β Type} (getElem : {n m : β} β Ξ± n m β β β β β β) (setElem : {n m : β} β Ξ± n m β β β β β β β Ξ± n m) (getValues : {n m : β} β Ξ± n m β List (β Γ β Γ β)) (ofValues : {n m : β} β List (β Γ β Γ β) β Ξ± n m) (swapRows : {n m : β} β Ξ± n m β β β β β Ξ± n m) (subtractRow : {n m : β} β Ξ± n m β β β β β β β Ξ± n m) (divideRow : {n m : β} β Ξ± n m β β β β β Ξ± n m) : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Ξ± - Linarith.SimplexAlgorithm.extractSolution π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
{matType : β β β β Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (tableau : Linarith.SimplexAlgorithm.Tableau matType) : Array β - Linarith.SimplexAlgorithm.findPositiveVector π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
{n m : β} {matType : β β β β Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (A : matType n m) (strictIndexes : List β) : Lean.MetaM (Array β) - Linarith.SimplexAlgorithm.postprocess π Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
(vec : Array β) : Std.HashMap β β - Rat.addCommGroup π Mathlib.Data.Rat.Defs
: AddCommGroup β - Rat.addCommMonoid π Mathlib.Data.Rat.Defs
: AddCommMonoid β
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. 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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
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.
This is Loogle revision 19971e9 serving mathlib revision 151dd12