name stringlengths 2 347 | module stringlengths 6 90 | type stringlengths 1 5.42M | docString stringlengths 0 11.5k ⌀ | allowCompletion bool 2
classes |
|---|---|---|---|---|
List.pairwise_le_finRange | Batteries.Data.List.Lemmas | ∀ (n : ℕ), List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.finRange n) | null | true |
HahnSeries.cardSuppLTAddSubgroup | Mathlib.RingTheory.HahnSeries.Cardinal | (Γ : Type u_1) →
(R : Type u_2) →
(κ : Cardinal.{u_1}) →
[inst : PartialOrder Γ] → [inst_1 : AddGroup R] → [hκ : Fact (Cardinal.aleph0 ≤ κ)] → AddSubgroup (HahnSeries Γ R) | The `κ`-bounded subgroup of Hahn series with less than `κ` terms. | true |
ProbabilityTheory.mgf_congr_identDistrib | Mathlib.Probability.Moments.Basic | ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
{mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ},
ProbabilityTheory.IdentDistrib X Y μ μ' → ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' | null | true |
CompositionAsSet.length.eq_1 | Mathlib.Combinatorics.Enumerative.Composition | ∀ {n : ℕ} (c : CompositionAsSet n), c.length = c.boundaries.card - 1 | null | true |
VAddCon._sizeOf_inst | Mathlib.Algebra.Module.Congruence.Defs | (S : Type u_2) → (M : Type u_3) → {inst : VAdd S M} → [SizeOf S] → [SizeOf M] → SizeOf (VAddCon S M) | null | false |
Filter.Tendsto.units._proof_1 | Mathlib.Topology.Algebra.Monoid | ∀ {ι : Type u_2} {N : Type u_1} [inst : TopologicalSpace N] [inst_1 : Monoid N] [ContinuousMul N] [T2Space N]
{f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot],
Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁) → Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂) → r₁ * r₂ = 1 | null | false |
Lean.Parser.Tactic.ImpossibleConfig.recOn | Init.Tactics | {motive : Lean.Parser.Tactic.ImpossibleConfig → Sort u} →
(t : Lean.Parser.Tactic.ImpossibleConfig) → ((levels : Bool) → motive { levels := levels }) → motive t | null | false |
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.response.elim | Std.Http.Server.Connection | {β : Type} →
{motive : Std.Http.Server.Connection.Recv✝ β → Sort u} →
(t : Std.Http.Server.Connection.Recv✝ β) →
Std.Http.Server.Connection.Recv.ctorIdx✝ t = 3 →
((x : Except IO.Error (Std.Http.Response β)) → motive (Std.Http.Server.Connection.Recv.response✝ x)) → motive t | null | false |
OrderIso.sumLexIicIoi_symm_apply_Iic | Mathlib.Order.Hom.Lex | ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Iic x)), (OrderIso.sumLexIicIoi x).symm ↑a = Sum.inl a | null | true |
Lean.Meta.Grind.UnitLike.State.ctorIdx | Lean.Meta.Tactic.Grind.Types | Lean.Meta.Grind.UnitLike.State → ℕ | null | false |
ProofWidgets.Html._sizeOf_1 | ProofWidgets.Data.Html | ProofWidgets.Html → ℕ | null | false |
CommMonoidWithZero.rec | Mathlib.Algebra.GroupWithZero.Defs | {M₀ : Type u_2} →
{motive : CommMonoidWithZero M₀ → Sort u} →
([toCommMonoid : CommMonoid M₀] →
[toZero : Zero M₀] →
(zero_mul : ∀ (a : M₀), 0 * a = 0) →
(mul_zero : ∀ (a : M₀), a * 0 = 0) →
motive { toCommMonoid := toCommMonoid, toZero := toZero, zero_mul := zero_mul, ... | null | false |
GrpCat.ext_iff | Mathlib.Algebra.Category.Grp.Basic | ∀ {X Y : GrpCat} {f g : X ⟶ Y},
f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x | null | true |
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_top_pos._simp_1_9 | Mathlib.Topology.Instances.EReal.Lemmas | ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a < max b c) = (a < b ∨ a < c) | null | false |
ModN.natCard_eq | Mathlib.LinearAlgebra.FreeModule.ModN | ∀ (G : Type u_1) [inst : AddCommGroup G] (n : ℕ) [NeZero n] [Module.Free ℤ G] [Module.Finite ℤ G],
Nat.card (ModN G n) = n ^ Module.finrank ℤ G | null | true |
CategoryTheory.MonoidalCategory.prodMonoidal._proof_15 | Mathlib.CategoryTheory.Monoidal.Category | ∀ (C₁ : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
(C₂ : Type u_2) [inst_2 : CategoryTheory.Category.{u_4, u_2} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
{X Y : C₁ × C₂} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Prod.m... | null | false |
Algebra.traceMatrix_reindex | Mathlib.RingTheory.Trace.Basic | ∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
{κ' : Type u_7} (b : Module.Basis κ A B) (f : κ ≃ κ'),
Algebra.traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (Algebra.traceMatrix A ⇑b) | null | true |
Algebra.instCompleteLatticeSubalgebra | Mathlib.Algebra.Algebra.Subalgebra.Lattice | {R : Type u} →
{A : Type v} →
[inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → CompleteLattice (Subalgebra R A) | null | true |
CategoryTheory.Limits.Cone.extendHom_hom | Mathlib.CategoryTheory.Limits.Cones | ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt), (s.extendHom f).hom = f | null | true |
Matrix.vecMulBilin._proof_6 | Mathlib.LinearAlgebra.Matrix.ToLin | ∀ {m : Type u_1} {n : Type u_2} (R : Type u_4) {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
[inst_2 : Module R A] [inst_3 : Fintype m] (x : R) (x_1 : m → A) (x_2 x_3 : Matrix m n A),
Matrix.vecMul (x • x_1) (x_2 + x_3) = Matrix.vecMul (x • x_1) x_2 + Matrix.vecMul (x • x_1) x_3 | null | false |
CategoryTheory.Mon.Hom.mk.sizeOf_spec | Mathlib.CategoryTheory.Monoidal.Mon | ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{M N : CategoryTheory.Mon C} [inst_2 : SizeOf C] (hom : M.X ⟶ N.X) [isMonHom_hom : CategoryTheory.IsMonHom hom],
sizeOf { hom := hom, isMonHom_hom := isMonHom_hom } = 1 + sizeOf hom + sizeOf isMonHom_hom | null | true |
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.Model.matchesAt_iff_exists_isMatch._simp_1_5 | Init.Data.String.Lemmas.Pattern.Basic | ∀ {s : String.Slice} {p : s.Pos} {q r : (s.sliceFrom p).Pos},
(q ≤ r) = (String.Slice.Pos.ofSliceFrom q ≤ String.Slice.Pos.ofSliceFrom r) | null | false |
truncSigmaOfExists._proof_1 | Mathlib.Data.Fintype.Basic | ∀ {α : Type u_1} {P : α → Prop}, (∃ a, P a) → Nonempty ((a : α) ×' P a) | null | false |
Int.add_neg | Init.Data.Int.Order | ∀ {a b : ℤ}, a < 0 → b < 0 → a + b < 0 | null | true |
Lean.Elab.Tactic.nonempty_to_inhabited | Mathlib.Tactic.Inhabit | (α : Sort u_1) → Nonempty α → Inhabited α | Derives `Inhabited α` from `Nonempty α` with `Classical.choice`. | true |
AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme | Mathlib.AlgebraicGeometry.Morphisms.LocalIso | CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsLocalIso | null | true |
LieAlgebra.polyCharpoly_coeff_rank_ne_zero | Mathlib.Algebra.Lie.Rank | ∀ (R : Type u_1) (L : Type u_3) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R]
[inst_7 : DecidableEq ι], ((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.r... | null | true |
Lean.Elab.Tactic.Do.Fuel.recOn | Lean.Elab.Tactic.Do.VCGen.Basic | {motive : Lean.Elab.Tactic.Do.Fuel → Sort u} →
(t : Lean.Elab.Tactic.Do.Fuel) →
((n : ℕ) → motive (Lean.Elab.Tactic.Do.Fuel.limited n)) → motive Lean.Elab.Tactic.Do.Fuel.unlimited → motive t | null | false |
NonemptyChain.rec | Mathlib.Order.BourbakiWitt | {α : Type u_4} →
[inst : LE α] →
{motive : NonemptyChain α → Sort u} →
((carrier : Set α) →
(Nonempty' : carrier.Nonempty) →
(isChain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier) →
motive { carrier := carrier, Nonempty' := Nonempty', isChain' := isChain' }) →
(t : N... | null | false |
CategoryTheory.BasedCategory.whiskerLeft_toNatTrans | Mathlib.CategoryTheory.FiberedCategory.BasedCategory | ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
{𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴)
{G H : CategoryTheory.BasedFunctor 𝒴 𝒵} (α : G ⟶ H),
(CategoryTheory.BasedCategory.whiskerLef... | null | true |
Int.instTransLe | Init.Data.Int.Order | Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 | null | true |
Lean.Order.iSup | Std.Internal.Do.Assertion | {α : Type u} → [Lean.Order.CompleteLattice α] → {ι : Type v} → (ι → α) → α | Indexed supremum | true |
List.forIn_map | Init.Data.List.Monadic | ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
{l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)},
forIn (List.map g l) init f = forIn l init fun a y => f (g a) y | null | true |
le_of_pow_le_pow_left₀ | Mathlib.Algebra.Order.GroupWithZero.Basic | ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ}
[MulPosMono M₀], n ≠ 0 → 0 ≤ b → a ^ n ≤ b ^ n → a ≤ b | null | true |
PadicAlgCl.valuation_p | Mathlib.NumberTheory.Padics.Complex | ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Valued.v ↑p = 1 / ↑p | The valuation of `p : PadicAlgCl p` is `1/p`. | true |
Nat.map_cast_int_atTop | Mathlib.Order.Filter.AtTopBot.Basic | Filter.map Nat.cast Filter.atTop = Filter.atTop | null | true |
QuotientGroup.mk_mul | Mathlib.GroupTheory.QuotientGroup.Defs | ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a b : G), ↑(a * b) = ↑a * ↑b | null | true |
Left.neg_lt_self | Mathlib.Algebra.Order.Group.Unbundled.Basic | ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a : α}, 0 < a → -a < a | null | true |
Std.DTreeMap.contains_emptyc | Std.Data.DTreeMap.Lemmas | ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false | null | true |
Finset.weightedVSub | Mathlib.LinearAlgebra.AffineSpace.Combination | {k : Type u_1} →
{V : Type u_2} →
{P : Type u_3} →
[inst : Ring k] →
[inst_1 : AddCommGroup V] →
[inst_2 : Module k V] → [S : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → (ι → k) →ₗ[k] V | A weighted sum of the results of subtracting a default base point
from the given points, as a linear map on the weights. This is
intended to be used when the sum of the weights is 0; that condition
is specified as a hypothesis on those lemmas that require it. | true |
_private.Mathlib.Tactic.ClickSuggestions.Util.0.Mathlib.Tactic.ClickSuggestions.mergeTactics?.match_1 | Mathlib.Tactic.ClickSuggestions.Util | (motive : Option (Lean.TSyntax `tactic) → Sort u_1) →
(__do_lift : Option (Lean.TSyntax `tactic)) →
((tac : Lean.TSyntax `tactic) → motive (some tac)) →
((x : Option (Lean.TSyntax `tactic)) → motive x) → motive __do_lift | null | false |
CategoryTheory.MorphismProperty.LeftFraction.unop_f | Mathlib.CategoryTheory.Localization.CalculusOfFractions | ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
(φ : W.LeftFraction X Y), φ.unop.f = φ.f.unop | null | true |
MeasureTheory.AddContent.mk._flat_ctor | Mathlib.MeasureTheory.Measure.AddContent | {α : Type u_1} →
{G : Type u_2} →
[inst : AddCommMonoid G] →
{C : Set (Set α)} →
(toFun : Set α → G) →
toFun ∅ = 0 →
(∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u) →
MeasureTheory.AddContent G C | null | false |
CommRingCat.commRingObj._proof_6 | Mathlib.Algebra.Category.Ring.Limits | ∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J CommRingCat) (j : J)
(a : (F.comp (CategoryTheory.forget CommRingCat)).obj j), 0 + a = a | null | false |
_private.Mathlib.Tactic.Linarith.Preprocessing.0.Mathlib.Tactic.Linarith.nlinarithGetSquareProofs | Mathlib.Tactic.Linarith.Preprocessing | List Lean.Expr → Lean.MetaM (List Lean.Expr) | Get proofs of `-x^2 ≤ 0` and `-(x*x) ≤ 0`, when those terms appear in `ls` | true |
BitVec.equivFin._proof_1 | Mathlib.Data.BitVec | ∀ {m : ℕ}, Function.LeftInverse (fun a => { toFin := a }) fun a => a.toFin | null | false |
Int.natCast_toNat_eq_self | Init.Data.Int.LemmasAux | ∀ {a : ℤ}, ↑a.toNat = a ↔ 0 ≤ a | null | true |
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_4 | Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound | ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
(c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
(pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
(ratHints : Array (ℕ × Array ℕ)) (h_1 : Unit → motive none)
... | null | true |
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital.0._auto_664 | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital | Lean.Syntax | null | false |
EReal.neg_mul | Mathlib.Data.EReal.Operations | ∀ (x y : EReal), -x * y = -(x * y) | null | true |
Bundle.Pretrivialization.continuousAlternatingMap._proof_5 | Mathlib.Topology.VectorBundle.ContinuousAlternatingMap | ∀ (𝕜 : Type u_7) (ι : Type u_1) [inst : NontriviallyNormedField 𝕜] {B : Type u_2} [inst_1 : TopologicalSpace B]
{F₁ : Type u_6} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_3}
[inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
[inst_6 : TopologicalSp... | null | false |
Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert | Mathlib.Analysis.Calculus.VectorField | ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
V₁ =ᶠ[nhdsWithin x (insert x s)] V →
W₁ =ᶠ[nhdsWithin x (insert x s)] W →
VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBra... | null | true |
Lean.AxiomVal.isUnsafeEx | Lean.Declaration | Lean.AxiomVal → Bool | null | true |
BitVec.not_or_self | Init.Data.BitVec.Lemmas | ∀ {w : ℕ} (x : BitVec w), ~~~x ||| x = BitVec.allOnes w | null | true |
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabLetE._sparseCasesOn_3 | Lean.PrettyPrinter.Delaborator.Builtins | {motive : Lean.Expr → Sort u} →
(t : Lean.Expr) →
((declName : Lean.Name) →
(type value body : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName type value body nondep)) →
(Nat.hasNotBit 256 t.ctorIdx → motive t) → motive t | null | false |
Std.ExtDHashMap.getKey?_inter_of_not_mem_left | Std.Data.ExtDHashMap.Lemmas | ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
[inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none | null | true |
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.splitStr._proof_1 | Lean.Server.FileWorker.SemanticHighlighting | ∀ (text : Lean.FileMap) (pos : String.Pos.Raw),
∀ i ∈ [(text.toPosition pos).line:text.positions.size], i < text.positions.size | null | false |
Pi.intCast_def | Mathlib.Data.Int.Cast.Pi | ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → IntCast (π i)] (n : ℤ), ↑n = fun x => ↑n | null | true |
CategoryTheory.ObjectProperty.ColimitOfShape._sizeOf_1 | Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape | {C : Type u_1} →
{inst : CategoryTheory.Category.{v_1, u_1} C} →
{P : CategoryTheory.ObjectProperty C} →
{J : Type u'} →
{inst_1 : CategoryTheory.Category.{v', u'} J} →
{X : C} → [SizeOf C] → [(a : C) → SizeOf (P a)] → [SizeOf J] → P.ColimitOfShape J X → ℕ | null | false |
Lean.Lsp.FoldingRangeParams.mk.sizeOf_spec | Lean.Data.Lsp.LanguageFeatures | ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument | null | true |
mul_self_nonneg | Mathlib.Algebra.Order.Ring.Unbundled.Basic | ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R),
0 ≤ a * a | null | true |
Std.IdempotentOp.idempotent | Init.Core | ∀ {α : Sort u} {op : α → α → α} [self : Std.IdempotentOp op] (x : α), op x x = x | An idempotent operation satisfies `a ∘ a = a`. | true |
Matroid.comap_isBasis'_iff._simp_1 | Mathlib.Combinatorics.Matroid.Map | ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {I X : Set α},
(N.comap f).IsBasis' I X = (N.IsBasis' (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X) | null | false |
LinearEquiv.conjAlgEquiv | Mathlib.Algebra.Algebra.Equiv | (R : Type u_1) →
{S : Type u_2} →
{M₁ : Type u_3} →
{M₂ : Type u_4} →
[inst : CommSemiring R] →
[inst_1 : AddCommMonoid M₁] →
[inst_2 : Module R M₁] →
[inst_3 : AddCommMonoid M₂] →
[inst_4 : Module R M₂] →
[inst_5 : Semiring S] →
... | A linear equivalence of two modules induces an equivalence of algebras of their
endomorphisms. | true |
_private.Init.Data.Order.PackageFactories.0.Std.LinearPreorderPackage.ofOrd._simp_4 | Init.Data.Order.PackageFactories | ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] {a b : α}, ((compare a b).isGE = true) = (b ≤ a) | null | false |
CategoryTheory.IsoCat.noConfusion | Mathlib.CategoryTheory.IsoCat | {P : Sort u} →
{C : Type u_1} →
{D : Type u_2} →
{inst : CategoryTheory.Category.{v_1, u_1} C} →
{inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
{t : CategoryTheory.IsoCat C D} →
{C' : Type u_1} →
{D' : Type u_2} →
{inst' : CategoryTheory.Categor... | null | false |
Ordinal.deriv_zero_left | Mathlib.SetTheory.Ordinal.FixedPoint | ∀ (a : Ordinal.{u_1}), Ordinal.deriv 0 a = a | null | true |
CategoryTheory.Monad.monadToMon._proof_2 | Mathlib.CategoryTheory.Monad.EquivMon | ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : CategoryTheory.Monad C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f.toNatTrans = CategoryTheory.MonObj.one | null | false |
HahnModule.instSMulZeroClass | Mathlib.RingTheory.HahnSeries.Multiplication | {Γ : Type u_1} →
{Γ' : Type u_2} →
{R : Type u_3} →
{V : Type u_5} →
[inst : PartialOrder Γ] →
[inst_1 : PartialOrder Γ'] →
[inst_2 : VAdd Γ Γ'] →
[IsOrderedCancelVAdd Γ Γ'] →
[inst_4 : AddCommMonoid V] →
[inst_5 : Zero R] → [inst... | null | true |
SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph._proof_1 | Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite | ∀ {r t : ℕ} {a b : Fin r × Fin t},
(SimpleGraph.completeMultipartiteGraph (Function.const (Fin r) (Fin t))).Adj
((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm a) ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm b) ↔
(SimpleGraph.completeEquipartiteGraph r t).Adj a b | null | false |
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.size_eq_if_roc._simp_1_2 | Init.Data.Range.Polymorphic.Lemmas | ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxc.HasSize α]
[Std.Rxc.LawfulHasSize α] {lo hi : α}, (Std.Rxc.HasSize.size lo hi = 0) = ¬lo ≤ hi | null | false |
HasMFDerivAt.mdifferentiableAt | Mathlib.Geometry.Manifold.MFDeriv.Basic | ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddComm... | null | true |
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst._proof_2 | Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong | ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
(X Y : C) {X_1 Y_1 : CategoryTheory.Over X} (g : X_1 ⟶ Y_1),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Over.Hom.left g) Y)
(Ca... | null | false |
AddMonoidAlgebra.ofMagma | Mathlib.Algebra.MonoidAlgebra.Defs | (R : Type u_8) → (M : Type u_9) → [inst : Semiring R] → [inst_1 : Add M] → Multiplicative M →ₙ* AddMonoidAlgebra R M | The embedding of an additive magma into its additive magma algebra. | true |
CategoryTheory.Aut.autMulEquivOfIso._proof_13 | Mathlib.CategoryTheory.Endomorphism | ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} (h : X ≅ Y) (x y : CategoryTheory.Aut X),
{ hom := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp (x * y).hom h.hom),
inv := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp (x * y)... | null | false |
MonoidWithZeroHom.funLike._proof_1 | Mathlib.Algebra.GroupWithZero.Hom | ∀ {α : Type u_1} {β : Type u_2} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f g : α →*₀ β),
(fun f => (↑f).toFun) f = (fun f => (↑f).toFun) g → f = g | null | false |
Lean.Grind.Linarith.lt_norm | Init.Grind.Ordered.Linarith | ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
[inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
(lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
Lean.Grind.Linarith.norm_cert lhs rhs p = true →
... | null | true |
Nonneg.one | Mathlib.Algebra.Order.Nonneg.Basic | {α : Type u_1} → [inst : Zero α] → [inst_1 : One α] → [inst_2 : LE α] → [ZeroLEOneClass α] → One { x // 0 ≤ x } | null | true |
DomMulAct.instCancelCommMonoidOfMulOpposite.eq_1 | Mathlib.GroupTheory.GroupAction.DomAct.Basic | ∀ {M : Type u_1} [inst : CancelCommMonoid Mᵐᵒᵖ], DomMulAct.instCancelCommMonoidOfMulOpposite = inst | null | true |
Nondet.bind.match_3 | Batteries.Control.Nondet.Basic | {σ : Type} →
{m : Type → Type} →
{α : Type} →
(motive : Option ((α × σ) × MLList m (α × σ)) → Sort u_1) →
(__do_lift : Option ((α × σ) × MLList m (α × σ))) →
(Unit → motive none) →
((x : α) → (s : σ) → (xs : MLList m (α × σ)) → motive (some ((x, s), xs))) → motive __do_lift | null | false |
instRingFreeRing._proof_31 | Mathlib.RingTheory.FreeRing | ∀ (α : Type u_1), autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam | null | false |
Lean.Grind.CommRing.Poly.degree | Lean.Meta.Sym.Arith.Poly | Lean.Grind.CommRing.Poly → ℕ | null | true |
SSet.horn.IsCompatible.δ_pred_comp._auto_1 | Mathlib.AlgebraicTopology.SimplicialSet.HornColimits | Lean.Syntax | null | false |
Std.Http.URI.Query.get | Std.Http.Data.URI.Basic | Std.Http.URI.Query → String → Option String | Gets the first value of a query parameter by key name, decoded as a string.
Returns `none` if the key is not found or if the value cannot be decoded as UTF-8.
| true |
RBTree.RBNode.Slow.instDecidableMemP | BatteriesRecycling.RBTree.Basic | {α : Type u_1} → {cut : α → Ordering} → {t : RBTree.RBNode α} → Decidable (RBTree.RBNode.MemP cut t) | null | true |
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.unifTight_of_tendsto_Lp | Mathlib.MeasureTheory.Function.UnifTight | ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
{p : ENNReal} {f : ℕ → α → β} {g : α → β},
p ≠ ⊤ →
(∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
MeasureTheory.MemLp g p μ →
Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p... | Convergence in Lp implies uniform tightness. | true |
Lean.Meta.Simp.registerBuiltinSimproc | Lean.Meta.Tactic.Simp.Simproc | Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.Simproc → IO Unit | null | true |
SimpleGraph.Copy.isoSubgraphMap._simp_3 | Mathlib.Combinatorics.SimpleGraph.Copy | ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, p a ∧ a = a') = p a' | null | false |
Qq.Impl.unquoteExpr | Qq.Macro | Lean.Expr → Qq.Impl.UnquoteM Lean.Expr | null | true |
_private.Mathlib.Data.Sign.Basic.0.sign_sum._simp_1_1 | Mathlib.Data.Sign.Basic | ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, (SignType.sign a = 0) = (a = 0) | null | false |
TopologicalSpace.CompactOpens.instInf._proof_1 | Mathlib.Topology.Sets.Compacts | ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] (U V : TopologicalSpace.CompactOpens α),
IsCompact (U.carrier ∩ V.carrier) | null | false |
ZeroAtInftyContinuousMap.instStarModule | Mathlib.Topology.ContinuousMap.ZeroAtInfty | ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {𝕜 : Type u_2} [inst_1 : Zero 𝕜] [inst_2 : Star 𝕜]
[inst_3 : AddMonoid β] [inst_4 : StarAddMonoid β] [inst_5 : TopologicalSpace β] [inst_6 : ContinuousStar β]
[inst_7 : SMulWithZero 𝕜 β] [inst_8 : ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β],
StarModule �... | null | true |
CategoryTheory.Limits.CategoricalPullback.mkIso._proof_3 | Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic | ∀ {A : Type u_3} {B : Type u_6} {C : Type u_4} [inst : CategoryTheory.Category.{u_1, u_3} A]
[inst_1 : CategoryTheory.Category.{u_5, u_6} B] [inst_2 : CategoryTheory.Category.{u_2, u_4} C]
{F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
{x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ :... | null | false |
_private.Mathlib.RingTheory.Valuation.Extension.0.Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff._simp_1_1 | Mathlib.RingTheory.Valuation.Extension | ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (x : R),
(x ∈ IsLocalRing.maximalIdeal R) = (x ∈ nonunits R) | null | false |
PseudoEpimorphism.comp_apply | Mathlib.Topology.Order.Hom.Esakia | ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
(g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) (a : α), (g.comp f) a = g (f a) | null | true |
_private.Lean.Meta.Tactic.Grind.Parser.0.Lean.Parser.Command.grindPattern._regBuiltin.Lean.Parser.Command.grindPatternCnstrs.parenthesizer_123 | Lean.Meta.Tactic.Grind.Parser | IO Unit | null | false |
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality | Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField | ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))
(AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) =
CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤)) (X.Γeval... | null | true |
_private.Mathlib.Topology.Algebra.Module.LinearPMap.0.LinearPMap.inverse_isClosable_iff.match_1_1 | Mathlib.Topology.Algebra.Module.LinearPMap | ∀ {R : Type u_1} {E : Type u_3} {F : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
[inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
{f : E →ₗ.[R] F} [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalS... | null | false |
CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ | Mathlib.Algebra.Homology.ShortComplex.LeftHomology | ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp S.toCycles S.leftHomologyπ = 0 | null | true |
NFA.Path.supp._sunfold | Mathlib.Computability.NFA | {α : Type u} → {σ : Type v} → {M : NFA α σ} → [DecidableEq σ] → {s t : σ} → {x : List α} → M.Path s t x → Finset σ | null | false |
End of preview. Expand in Data Studio
Mathlib Types
This dataset contains information about types defined in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
fabf563a7c95a166b8d7b6efca11c8b4dc9d911f
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: false
name: name
- type:
datatype: string
nullable: true
name: module
- type:
datatype: string
nullable: false
name: type
- type:
datatype: string
nullable: true
name: docString
- type:
datatype: bool
nullable: false
name: allowCompletion
Attribution
This dataset is derived from Mathlib, an open-source mathematical library developed by the leanprover-community. If you use this dataset, please cite the Mathlib paper or the Mathlib repository.
A full list of Mathlib contributors is available at: https://github.com/leanprover-community/mathlib4/graphs/contributors
- Downloads last month
- 827