Loogle!

Result

Found 169 declarations mentioning PNat.val.

• PNat.val 📋 Mathlib.Data.PNat.Notation
  : ℕ+ → ℕ
• PNat.coe_injective 📋 Mathlib.Data.PNat.Defs
  : Function.Injective PNat.val
• PNat.coe_toPNat' 📋 Mathlib.Data.PNat.Defs
  (n : ℕ+) : (↑n).toPNat' = n
• Nat.succPNat_coe 📋 Mathlib.Data.PNat.Defs
  (n : ℕ) : ↑n.succPNat = n.succ
• NeZero.pnat 📋 Mathlib.Data.PNat.Defs
  {a : ℕ+} : NeZero ↑a
• PNat.ne_zero 📋 Mathlib.Data.PNat.Defs
  (n : ℕ+) : ↑n ≠ 0
• PNat.pos 📋 Mathlib.Data.PNat.Defs
  (n : ℕ+) : 0 < ↑n
• PNat.eq 📋 Mathlib.Data.PNat.Defs
  {m n : ℕ+} : ↑m = ↑n → m = n
• Nat.canLiftPNat 📋 Mathlib.Data.PNat.Defs
  : CanLift ℕ ℕ+ PNat.val fun n => 0 < n
• PNat.toPNat'_coe 📋 Mathlib.Data.PNat.Defs
  {n : ℕ} : 0 < n → ↑n.toPNat' = n
• Int.canLiftPNat 📋 Mathlib.Data.PNat.Defs
  : CanLift ℤ ℕ+ (fun x => ↑↑x) fun x => 0 < x
• PNat.one_coe 📋 Mathlib.Data.PNat.Defs
  : ↑1 = 1
• PNat.coe_le_coe 📋 Mathlib.Data.PNat.Defs
  (n k : ℕ+) : ↑n ≤ ↑k ↔ n ≤ k
• PNat.coe_lt_coe 📋 Mathlib.Data.PNat.Defs
  (n k : ℕ+) : ↑n < ↑k ↔ n < k
• PNat.coe_eq_one_iff 📋 Mathlib.Data.PNat.Defs
  {m : ℕ+} : ↑m = 1 ↔ m = 1
• PNat.mk_coe 📋 Mathlib.Data.PNat.Defs
  (n : ℕ) (h : 0 < n) : ↑⟨n, h⟩ = n
• Nat.toPNat'_coe 📋 Mathlib.Data.PNat.Defs
  (n : ℕ) : ↑n.toPNat' = if 0 < n then n else 1
• PNat.mod_coe 📋 Mathlib.Data.PNat.Defs
  (m k : ℕ+) : ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
• PNat.div_coe 📋 Mathlib.Data.PNat.Defs
  (m k : ℕ+) : m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k
• Rat.coe_pnatDen 📋 Mathlib.Data.Rat.Lemmas
  (x : ℚ) : ↑x.pnatDen = x.den
• Rat.pnatDen_eq_iff_den_eq 📋 Mathlib.Data.Rat.Lemmas
  {x : ℚ} {n : ℕ+} : x.pnatDen = n ↔ x.den = ↑n
• PNat.coe_inj 📋 Mathlib.Data.PNat.Basic
  {m n : ℕ+} : ↑m = ↑n ↔ m = n
• PNat.pos_of_div_pos 📋 Mathlib.Data.PNat.Basic
  {n : ℕ+} {a : ℕ} (h : a ∣ ↑n) : 0 < a
• PNat.natPred_add_one 📋 Mathlib.Data.PNat.Basic
  (n : ℕ+) : n.natPred + 1 = ↑n
• PNat.one_add_natPred 📋 Mathlib.Data.PNat.Basic
  (n : ℕ+) : 1 + n.natPred = ↑n
• PNat.lt_succ_self 📋 Mathlib.Data.PNat.Basic
  (a : ℕ+) : a < (↑a).succPNat
• PNat.coeAddHom_apply 📋 Mathlib.Data.PNat.Basic
  (a✝ : ℕ+) : PNat.coeAddHom a✝ = ↑a✝
• PNat.dvd_iff 📋 Mathlib.Data.PNat.Basic
  {k m : ℕ+} : k ∣ m ↔ ↑k ∣ ↑m
• PNat.val_ofNat 📋 Mathlib.Data.PNat.Basic
  (n : ℕ) [NeZero n] : ↑(OfNat.ofNat n) = OfNat.ofNat n
• PNat.add_coe 📋 Mathlib.Data.PNat.Basic
  (m n : ℕ+) : ↑(m + n) = ↑m + ↑n
• PNat.add_one 📋 Mathlib.Data.PNat.Basic
  (a : ℕ+) : a + 1 = (↑a).succPNat
• PNat.mul_coe 📋 Mathlib.Data.PNat.Basic
  (m n : ℕ+) : ↑(m * n) = ↑m * ↑n
• PNat.div_add_mod 📋 Mathlib.Data.PNat.Basic
  (m k : ℕ+) : ↑k * m.div k + ↑(m.mod k) = ↑m
• PNat.div_add_mod' 📋 Mathlib.Data.PNat.Basic
  (m k : ℕ+) : m.div k * ↑k + ↑(m.mod k) = ↑m
• PNat.mod_add_div 📋 Mathlib.Data.PNat.Basic
  (m k : ℕ+) : ↑(m.mod k) + ↑k * m.div k = ↑m
• PNat.mod_add_div' 📋 Mathlib.Data.PNat.Basic
  (m k : ℕ+) : ↑(m.mod k) + m.div k * ↑k = ↑m
• PNat.coe_coeMonoidHom 📋 Mathlib.Data.PNat.Basic
  : ⇑PNat.coeMonoidHom = PNat.val
• PNat.pow_coe 📋 Mathlib.Data.PNat.Basic
  (m : ℕ+) (n : ℕ) : ↑(m ^ n) = ↑m ^ n
• PNat.sub_coe 📋 Mathlib.Data.PNat.Basic
  (a b : ℕ+) : ↑(a - b) = if b < a then ↑a - ↑b else 1
• PNat.modDivAux_spec 📋 Mathlib.Data.PNat.Basic
  (k : ℕ+) (r q : ℕ) : ¬(r = 0 ∧ q = 0) → ↑(k.modDivAux r q).1 + ↑k * (k.modDivAux r q).2 = r + ↑k * q
• Finset.PNat.coe_prod 📋 Mathlib.Algebra.Order.BigOperators.Ring.Finset
  {ι : Type u_4} (f : ι → ℕ+) (s : Finset ι) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
• PNat.isCoprime_iff 📋 Mathlib.RingTheory.Coprime.Basic
  {m n : ℕ+} : IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1
• Function.iUnion_pnat_ptsOfPeriod 📋 Mathlib.Dynamics.PeriodicPts.Defs
  {α : Type u_1} (f : α → α) : ⋃ n, Function.ptsOfPeriod f ↑n = Function.periodicPts f
• Function.directed_ptsOfPeriod_pnat 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} (f : α → α) : Directed (fun x1 x2 => x1 ⊆ x2) fun n => Function.ptsOfPeriod f ↑n
• ppow_eq_pow 📋 Mathlib.Algebra.Group.PNatPowAssoc
  {M : Type u_1} [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) : x ^ n = x ^ ↑n
• Filter.exists_lt_of_le_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : Filter.IsBoundedUnder GE.ge Filter.atTop u) (hu : x ≤ Filter.liminf u Filter.atTop) (hε : ε < 0) : ∃ n, x + ε < u ↑n
• Filter.exists_lt_of_limsup_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : Filter.IsBoundedUnder LE.le Filter.atTop u) (hu : Filter.limsup u Filter.atTop ≤ x) (hε : 0 < ε) : ∃ n, u ↑n < x + ε
• multipliable_pnat_iff_multipliable_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} : (Multipliable fun n => f ↑n) ↔ Multipliable f
• summable_pnat_iff_summable_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} : (Summable fun n => f ↑n) ↔ Summable f
• multipliable_pnat_iff_multipliable_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} : (Multipliable fun x => f ↑x) ↔ Multipliable fun x => f (x + 1)
• summable_pnat_iff_summable_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} : (Summable fun x => f ↑x) ↔ Summable fun x => f (x + 1)
• tprod_pnat_eq_tprod_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} : ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f (n + 1)
• tsum_pnat_eq_tsum_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} : ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f (n + 1)
• hasProd_pnat_iff_hasProd_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} {f : ℕ → M} : HasProd (fun x => f ↑x) m ↔ HasProd (fun x => f (x + 1)) m
• hasSum_pnat_iff_hasSum_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {f : ℕ → M} : HasSum (fun x => f ↑x) m ↔ HasSum (fun x => f (x + 1)) m
• tprod_pnat_eq_tprod_of_eq_one 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} (hf : f 0 = 1) : ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n
• tsum_pnat_eq_tsum_of_eq_zero 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} (hf : f 0 = 0) : ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
• hasProd_pnat_iff 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} {a : G} : HasProd (fun x => f ↑x) a ↔ HasProd f (a * f 0)
• hasSum_pnat_iff 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} {a : G} : HasSum (fun x => f ↑x) a ↔ HasSum f (a + f 0)
• tprod_zero_pnat_eq_tprod_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G} (hf : Multipliable f) : f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n
• tsum_zero_pnat_eq_tsum_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) : f 0 + ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
• tprod_int_eq_zero_mul_tprod_pnat_sq 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf : Function.Even f) (hf2 : Multipliable f) : ∏' (n : ℤ), f n = f 0 * (∏' (n : ℕ+), f ↑↑n) ^ 2
• tsum_int_eq_zero_add_two_mul_tsum_pnat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf : Function.Even f) (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + 2 • ∑' (n : ℕ+), f ↑↑n
• tprod_int_eq_zero_mul_tprod_pnat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf2 : Multipliable f) : ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f ↑↑n) * ∏' (n : ℕ+), f (-↑↑n)
• tsum_int_eq_zero_add_tsum_pnat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + ∑' (n : ℕ+), f ↑↑n + ∑' (n : ℕ+), f (-↑↑n)
• tendsto_PNat_val_atTop_atTop 📋 Mathlib.Order.Filter.AtTopBot.Archimedean
  : Filter.Tendsto PNat.val Filter.atTop Filter.atTop
• PNat.tendsto_comp_val_iff 📋 Mathlib.Order.Filter.AtTopBot.Archimedean
  {β : Type u_3} {f : ℕ → β} {l : Filter β} : Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
• PNat.equivNonZeroDivisorsNat_apply_coe 📋 Mathlib.Algebra.Order.Monoid.PNat
  (x : ℕ+) : ↑(PNat.equivNonZeroDivisorsNat x) = ↑x
• FiniteField.card 📋 Mathlib.FieldTheory.Finite.Basic
  (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [CharP K p] : ∃ n, Nat.Prime p ∧ Fintype.card K = p ^ ↑n
• FiniteField.card' 📋 Mathlib.FieldTheory.Finite.Basic
  (K : Type u_1) [Field K] [Fintype K] : ∃ p, CharP K p ∧ ∃ n, Nat.Prime p ∧ Fintype.card K = p ^ ↑n
• AlgebraicGeometry.Proj.affineOpenCover_f 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
  {σ : Type u_1} {A : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (i : (i : ℕ+) × ↥(𝒜 ↑i)) : (AlgebraicGeometry.Proj.affineOpenCover 𝒜).f i = AlgebraicGeometry.Proj.awayι 𝒜 ↑i.snd ⋯ ⋯
• AlgebraicGeometry.Proj.mapAffineOpenCover_f 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
  {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (i : (AlgebraicGeometry.Proj.affineOpenCover 𝒜).I₀) : (AlgebraicGeometry.Proj.mapAffineOpenCover f hf).f i = AlgebraicGeometry.Proj.awayι ℬ (f ↑i.snd) ⋯ ⋯
• Complex.UnitDisc.coe_pow 📋 Mathlib.Analysis.Complex.UnitDisc.Basic
  (z : Complex.UnitDisc) (n : ℕ+) : ↑(z ^ n) = ↑z ^ ↑n
• PNat.instFactPrimeValOfPrime 📋 Mathlib.Data.PNat.Prime
  {p : ℕ+} [h : Fact p.Prime] : Fact (Nat.Prime ↑p)
• PNat.coprime_coe 📋 Mathlib.Data.PNat.Prime
  {m n : ℕ+} : (↑m).Coprime ↑n ↔ m.Coprime n
• Nat.Primes.coe_pnat_nat 📋 Mathlib.Data.PNat.Prime
  (p : Nat.Primes) : ↑↑p = ↑p
• PNat.gcd_coe 📋 Mathlib.Data.PNat.Prime
  (n m : ℕ+) : ↑(n.gcd m) = (↑n).gcd ↑m
• PNat.lcm_coe 📋 Mathlib.Data.PNat.Prime
  (n m : ℕ+) : ↑(n.lcm m) = (↑n).lcm ↑m
• PNat.Coprime.pow 📋 Mathlib.Data.PNat.Prime
  {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (↑m ^ k).Coprime (↑n ^ l)
• Polynomial.unique_int_coeff_of_cycl 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
  {K : Type u_2} [CommRing K] [IsDomain K] [CharZero K] {ζ : K} {n : ℕ+} (h : IsPrimitiveRoot ζ ↑n) : ∃! P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' (↑n) K
• AddChar.primitiveZModChar 📋 Mathlib.NumberTheory.LegendreSymbol.AddCharacter
  (n : ℕ+) (F' : Type v) [Field F'] (h : ↑↑n ≠ 0) : AddChar.PrimitiveAddChar (ZMod ↑n) F'
• AddChar.PrimitiveAddChar.prim 📋 Mathlib.NumberTheory.LegendreSymbol.AddCharacter
  {R : Type u} [CommRing R] {R' : Type v} [Field R'] (self : AddChar.PrimitiveAddChar R R') : self.char.IsPrimitive
• AddChar.PrimitiveAddChar.mk 📋 Mathlib.NumberTheory.LegendreSymbol.AddCharacter
  {R : Type u} [CommRing R] {R' : Type v} [Field R'] (n : ℕ+) (char : AddChar R (CyclotomicField (↑n) R')) (prim : char.IsPrimitive) : AddChar.PrimitiveAddChar R R'
• AddChar.PrimitiveAddChar.char 📋 Mathlib.NumberTheory.LegendreSymbol.AddCharacter
  {R : Type u} [CommRing R] {R' : Type v} [Field R'] (self : AddChar.PrimitiveAddChar R R') : AddChar R (CyclotomicField (↑self.n) R')
• AddChar.val_mem_rootsOfUnity 📋 Mathlib.NumberTheory.LegendreSymbol.AddCharacter
  {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] (φ : AddChar R R') (a : R) (h : 0 < ringChar R) : ⋯.unit ∈ rootsOfUnity (↑(ringChar R).toPNat') R'
• smoothingSeminormSeq_bddBelow 📋 Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
  {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : BddBelow (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))
• smoothingFun_le 📋 Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
  {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) (n : ℕ+) : smoothingFun μ x ≤ μ (x ^ ↑n) ^ (1 / ↑↑n)
• zero_mem_lowerBounds_smoothingSeminormSeq_range 📋 Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
  {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : 0 ∈ lowerBounds (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))
• cot_series_rep 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hz : x ∈ Complex.integerComplement) : ↑Real.pi * (↑Real.pi * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))
• PrimeMultiset.coe_prod 📋 Mathlib.Data.PNat.Factors
  (v : PrimeMultiset) : ↑v.prod = v.toNatMultiset.prod
• PNat.coeNat_factorMultiset 📋 Mathlib.Data.PNat.Factors
  (n : ℕ+) : n.factorMultiset.toNatMultiset = ↑(↑n).primeFactorsList
• PrimeMultiset.coePNat_nat 📋 Mathlib.Data.PNat.Factors
  (v : PrimeMultiset) : Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset
• PrimeMultiset.prod_ofNatMultiset 📋 Mathlib.Data.PNat.Factors
  (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p) : ↑(PrimeMultiset.ofNatMultiset v h).prod = v.prod
• PrimeMultiset.prod_ofNatList 📋 Mathlib.Data.PNat.Factors
  (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p) : ↑(PrimeMultiset.ofNatList l h).prod = l.prod
• PrimeMultiset.mem_ofNatList 📋 Mathlib.Data.PNat.Factors
  {p : ℕ+} {l : List ℕ} (hl : ∀ p ∈ l, Nat.Prime p) : p ∈ (PrimeMultiset.ofNatList l hl).toPNatMultiset ↔ ↑p ∈ l
• PrimeMultiset.mem_ofNatMultiset 📋 Mathlib.Data.PNat.Factors
  {p : ℕ+} {s : Multiset ℕ} (hs : ∀ p ∈ s, Nat.Prime p) : p ∈ (PrimeMultiset.ofNatMultiset s hs).toPNatMultiset ↔ ↑p ∈ s
• PNat.decidablePredExistsNat 📋 Mathlib.Data.PNat.Find
  {p : ℕ+ → Prop} [DecidablePred p] : DecidablePred fun n' => ∃ n, ∃ (_ : n' = ↑n), p n
• PNat.card_Ico 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : (Finset.Ico a b).card = ↑b - ↑a
• PNat.card_Ioc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : (Finset.Ioc a b).card = ↑b - ↑a
• PNat.uIcc_eq_finset_subtype 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.uIcc a b = Finset.subtype (fun n => 0 < n) (Finset.uIcc ↑a ↑b)
• PNat.card_Icc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : (Finset.Icc a b).card = ↑b + 1 - ↑a
• PNat.card_Ioo 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : (Finset.Ioo a b).card = ↑b - ↑a - 1
• PNat.card_uIcc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : (Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
• PNat.Icc_eq_finset_subtype 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.Icc a b = Finset.subtype (fun n => 0 < n) (Finset.Icc ↑a ↑b)
• PNat.Ico_eq_finset_subtype 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.Ico a b = Finset.subtype (fun n => 0 < n) (Finset.Ico ↑a ↑b)
• PNat.Ioc_eq_finset_subtype 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.Ioc a b = Finset.subtype (fun n => 0 < n) (Finset.Ioc ↑a ↑b)
• PNat.Ioo_eq_finset_subtype 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.Ioo a b = Finset.subtype (fun n => 0 < n) (Finset.Ioo ↑a ↑b)
• PNat.card_fintype_Ico 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
• PNat.card_fintype_Ioc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
• PNat.map_subtype_embedding_uIcc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
• PNat.map_subtype_embedding_Icc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Icc a b) = Finset.Icc ↑a ↑b
• PNat.map_subtype_embedding_Ico 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ico a b) = Finset.Ico ↑a ↑b
• PNat.map_subtype_embedding_Ioc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
• PNat.map_subtype_embedding_Ioo 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
• PNat.card_fintype_uIcc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
• PNat.card_fintype_Icc 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
• PNat.card_fintype_Ioo 📋 Mathlib.Data.PNat.Interval
  (a b : ℕ+) : Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
• PNat.XgcdType.start_v 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : (PNat.XgcdType.start a b).v = (↑a, ↑b)
• PNat.gcdA'_coe 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : ↑(a.gcdA' b) = ↑(a.gcdW b) + a.gcdX b
• PNat.gcdB'_coe 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : ↑(a.gcdB' b) = a.gcdY b + ↑(a.gcdZ b)
• PNat.gcd_rel_left' 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
• PNat.gcd_rel_right' 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
• PNat.gcd_rel_left 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcd b)
• PNat.gcd_rel_right 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcd b)
• PNat.gcd_props 📋 Mathlib.Data.PNat.Xgcd
  (a b : ℕ+) : have d := a.gcdD b; have w := a.gcdW b; have x := a.gcdX b; have y := a.gcdY b; have z := a.gcdZ b; have a' := a.gcdA' b; have b' := a.gcdB' b; w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
• DivisibleHull.mk_eq_mk_iff_smul_eq_smul 📋 Mathlib.GroupTheory.DivisibleHull
  {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] {m m' : M} {s s' : ℕ+} : DivisibleHull.mk m s = DivisibleHull.mk m' s' ↔ ↑s' • m = ↑s • m'
• DivisibleHull.mk_le_mk 📋 Mathlib.GroupTheory.DivisibleHull
  {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] {m m' : M} {s s' : ℕ+} : DivisibleHull.mk m s ≤ DivisibleHull.mk m' s' ↔ ↑s' • m ≤ ↑s • m'
• DivisibleHull.mk_eq_mk 📋 Mathlib.GroupTheory.DivisibleHull
  {M : Type u_1} [AddCommMonoid M] {m m' : M} {s s' : ℕ+} : DivisibleHull.mk m s = DivisibleHull.mk m' s' ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'
• DivisibleHull.mk_lt_mk 📋 Mathlib.GroupTheory.DivisibleHull
  {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] {m m' : M} {s s' : ℕ+} : DivisibleHull.mk m s < DivisibleHull.mk m' s' ↔ ↑s' • m < ↑s • m'
• DivisibleHull.mk_add_mk 📋 Mathlib.GroupTheory.DivisibleHull
  {M : Type u_1} [AddCommMonoid M] {m1 m2 : M} {s1 s2 : ℕ+} : DivisibleHull.mk m1 s1 + DivisibleHull.mk m2 s2 = DivisibleHull.mk (↑s2 • m1 + ↑s1 • m2) (s1 * s2)
• ADEInequality.sumInv_pqr 📋 Mathlib.NumberTheory.ADEInequality
  (p q r : ℕ+) : ADEInequality.sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹
• NumberField.Units.rootsOfUnity_eq_one 📋 Mathlib.NumberTheory.NumberField.Units.Basic
  (K : Type u_1) [Field K] {k : ℕ+} (hc : (↑k).Coprime (NumberField.Units.torsionOrder K)) {ζ : (NumberField.RingOfIntegers K)ˣ} : ζ ∈ rootsOfUnity (↑k) (NumberField.RingOfIntegers K) ↔ ζ = 1
• LucasLehmer.ωUnit 📋 Mathlib.NumberTheory.LucasLehmer
  (p : ℕ) : (LucasLehmer.X ↑(LucasLehmer.q p))ˣ
• LucasLehmer.ωUnit_coe 📋 Mathlib.NumberTheory.LucasLehmer
  (p : ℕ) : ↑(LucasLehmer.ωUnit p) = LucasLehmer.X.ω
• LucasLehmer.mersenne_coe_X 📋 Mathlib.NumberTheory.LucasLehmer
  (p : ℕ) : ↑(mersenne p) = 0
• LucasLehmer.order_ineq 📋 Mathlib.NumberTheory.LucasLehmer
  (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : 2 ^ (p' + 2) < ↑(LucasLehmer.q (p' + 2)) ^ 2
• LucasLehmer.order_ω 📋 Mathlib.NumberTheory.LucasLehmer
  (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : orderOf (LucasLehmer.ωUnit (p' + 2)) = 2 ^ (p' + 2)
• LucasLehmer.ω_pow_eq_one 📋 Mathlib.NumberTheory.LucasLehmer
  (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : LucasLehmer.X.ω ^ 2 ^ (p' + 2) = 1
• LucasLehmer.ω_pow_eq_neg_one 📋 Mathlib.NumberTheory.LucasLehmer
  (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : LucasLehmer.X.ω ^ 2 ^ (p' + 1) = -1
• LucasLehmer.ω_pow_formula 📋 Mathlib.NumberTheory.LucasLehmer
  (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : ∃ k, LucasLehmer.X.ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * LucasLehmer.X.ω ^ 2 ^ p' - 1
• divisorsAntidiagonalFactors 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  (n : ℕ+) : ↥(↑n).divisorsAntidiagonal → ℕ+ × ℕ+
• sigmaAntidiagonalEquivProd 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  : (n : ℕ+) × ↥(↑n).divisorsAntidiagonal ≃ ℕ+ × ℕ+
• divisorsAntidiagonalFactors_eq 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  {n : ℕ+} (x : ↥(↑n).divisorsAntidiagonal) : ↑(divisorsAntidiagonalFactors n x).1 * ↑(divisorsAntidiagonalFactors n x).2 = ↑n
• tendsto_zero_geometric_tsum_pnat 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : Filter.Tendsto (fun m => ∑' (n : ℕ+), r ^ (↑n * ↑m)) Filter.atTop (nhds 0)
• summable_prod_mul_pow 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : Summable fun c => ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2)
• sigmaAntidiagonalEquivProd_symm_apply_fst 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).fst = ↑x.1 * ↑x.2
• tsum_prod_pow_eq_tsum_sigma 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((ArithmeticFunction.sigma k) ↑e) * r ^ ↑e
• tsum_pow_div_one_sub_eq_tsum_sigma 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ) : ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma k) ↑n) * r ^ ↑n
• sigmaAntidiagonalEquivProd_symm_apply_snd 📋 Mathlib.NumberTheory.TsumDivisorsAntidiagonal
  (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).snd = (↑x.1, ↑x.2)
• summable_pow_mul_cexp 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  (k : ℕ) (e : ℕ+) (z : UpperHalfPlane) : Summable fun c => ↑c ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑e * ↑z) ^ c
• EisensteinSeries.qExpansion_identity_pnat 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ+), ↑↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z = 2 * riemannZeta ↑k + 2 * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• EisensteinSeries.q_expansion_bernoulli 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : (ModularForm.E hk) z = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
• EisensteinSeries.q_expansion_riemannZeta 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : (ModularForm.E hk) z = 1 + (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
• EisensteinSeries.E2_eq_tsum_cexp 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : EisensteinSeries.E2 z = 1 - 24 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : Filter.Tendsto (fun N => ∑ n ∈ Finset.Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))
• EisensteinSeries.G2_eq_tsum_cexp 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : EisensteinSeries.G2 z = 2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• EisensteinSeries.hasSum_e2Summand_symmetricIcc 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : HasSum (fun x => EisensteinSeries.e2Summand x z) (2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n) (SummationFilter.symmetricIcc ℤ)
• EisensteinSeries.hasSum_e2Summand_symmetricIco 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : HasSum (fun x => EisensteinSeries.e2Summand x z) (2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n) (SummationFilter.symmetricIco ℤ)
• ONote.oadd_lt_oadd_2 📋 Mathlib.SetTheory.Ordinal.Notation
  {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+} (h₁ : (e.oadd n₁ o₁).NF) (h : ↑n₁ < ↑n₂) : e.oadd n₁ o₁ < e.oadd n₂ o₂
• ONote.repr_opow_aux₁ 📋 Mathlib.SetTheory.Ordinal.Notation
  {e a : ONote} [Ne : e.NF] [Na : a.NF] {a' : Ordinal.{0}} (e0 : e.repr ≠ 0) (h : a' < Ordinal.omega0 ^ e.repr) (aa : a.repr = a') (n : ℕ+) : (Ordinal.omega0 ^ e.repr * ↑↑n + a') ^ Ordinal.omega0 = (Ordinal.omega0 ^ e.repr) ^ Ordinal.omega0
• ONote.repr_opow_aux₂ 📋 Mathlib.SetTheory.Ordinal.Notation
  {a0 a' : ONote} [N0 : a0.NF] [Na' : a'.NF] (m : ℕ) (d : Ordinal.omega0 ∣ a'.repr) (e0 : a0.repr ≠ 0) (h : a'.repr + ↑m < Ordinal.omega0 ^ a0.repr) (n : ℕ+) (k : ℕ) : have R := (ONote.opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr; (k ≠ 0 → R < (Ordinal.omega0 ^ a0.repr) ^ Order.succ ↑k) ∧ (Ordinal.omega0 ^ a0.repr) ^ ↑k * (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr) + R = (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ Order.succ ↑k
• Mathlib.Tactic.PNatToNat.coe_inj 📋 Mathlib.Tactic.PNatToNat
  (m n : ℕ+) : m = n ↔ ↑m = ↑n
• Mathlib.Tactic.PNatToNat.coe_le_coe 📋 Mathlib.Tactic.PNatToNat
  (m n : ℕ+) : m ≤ n ↔ ↑m ≤ ↑n
• Mathlib.Tactic.PNatToNat.coe_lt_coe 📋 Mathlib.Tactic.PNatToNat
  (m n : ℕ+) : m < n ↔ ↑m < ↑n
• Mathlib.Tactic.PNatToNat.sub_coe 📋 Mathlib.Tactic.PNatToNat
  (a b : ℕ+) : ↑(a - b) = ↑a - 1 - ↑b + 1
• PNat.isUniformEmbedding_coe 📋 Mathlib.Topology.Instances.PNat
  : IsUniformEmbedding PNat.val
• PNat.dist_coe 📋 Mathlib.Topology.Instances.PNat
  (x y : ℕ+) : dist ↑x ↑y = dist x y
• PNat.dist_eq 📋 Mathlib.Topology.Instances.PNat
  (x y : ℕ+) : dist x y = |↑↑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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

5. 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