mathlib

swMATH36839MaRDI QIDQ52541FDOQ52541

Jump to:navigation, searchThe Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.

Author name not available (Why is that?)

Official website: https://leanprover-community.github.io

Source code repository: https://github.com/leanprover-community/mathlib

Described by source

• Maintaining a library of formal mathematics

Cited In (only showing first 100 items - show all)

• mathlib4 Module Mathlib/NumberTheory/KummerDedekind
• mathlib4 Module Mathlib/NumberTheory/RamificationInertia/Galois
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/AdicValuation
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/Basic
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/Dvr
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/IntegralClosure
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/SInteger
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/Ideal/Basic
• mathlib4 Module Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas
• mathlib4 Module Mathlib/NumberTheory/Ostrowski
• mathlib4 Module Mathlib/RingTheory/FractionalIdeal/Inverse
• mathlib4 Module Mathlib/NumberTheory/Pell
• mathlib4 Module Mathlib/NumberTheory/JacobiSum/Basic
• mathlib4 Module Mathlib/NumberTheory/SelbergSieve
• mathlib4 Module Mathlib/NumberTheory/SelbergSieve
• mathlib4 Module Mathlib/NumberTheory/SiegelsLemma
• mathlib4 Module Mathlib/NumberTheory/NumberField/House
• mathlib4 Module Mathlib/NumberTheory/Padics/MahlerBasis
• mathlib4 Module Mathlib/NumberTheory/Padics/PadicIntegers
• mathlib4 Module Mathlib/NumberTheory/Padics/PadicNorm
• mathlib4 Module Mathlib/NumberTheory/Padics/PadicNumbers
• mathlib4 Module Mathlib/NumberTheory/Padics/PadicVal/Basic
• mathlib4 Module Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected
• mathlib4 Module Mathlib/Order/BourbakiWitt
• mathlib4 Module Mathlib/Order/CompletePartialOrder
• mathlib4 Module Mathlib/Order/Concept
• mathlib4 Module Mathlib/Order/Concept
• mathlib4 Module Mathlib/Topology/Order/Priestley
• mathlib4 Module Mathlib/Order/Directed
• mathlib4 Module Mathlib/Order/ScottContinuity
• mathlib4 Module Mathlib/Topology/Order/HullKernel
• mathlib4 Module Mathlib/Topology/Order/Lattice
• mathlib4 Module Mathlib/Topology/Order/LawsonTopology
• mathlib4 Module Mathlib/Topology/Order/LowerUpperTopology
• mathlib4 Module Mathlib/Order/Grade
• mathlib4 Module Mathlib/Topology/Order/ScottTopology
• mathlib4 Module Mathlib/Order/Grade
• mathlib4 Module Mathlib/Order/OmegaCompletePartialOrder
• mathlib4 Module Mathlib/Order/OmegaCompletePartialOrder
• mathlib4 Module Mathlib/Order/Sublocale
• mathlib4 Module Mathlib/Topology/Order/Category/FrameAdjunction
• mathlib4 Module Mathlib/Order/WellFoundedSet
• mathlib4 Module Mathlib/Order/WellFoundedSet
• mathlib4 Module Mathlib/Order/BooleanAlgebra/Basic
• mathlib4 Module Mathlib/Order/BooleanAlgebra/Defs
• mathlib4 Module Mathlib/Order/CompactlyGenerated/Basic
• mathlib4 Module Mathlib/Probability/Distributions/Fernique
• mathlib4 Module Mathlib/Probability/Kernel/RadonNikodym
• mathlib4 Module Mathlib/Probability/Kernel/Disintegration/Density
• mathlib4 Module Mathlib/Probability/Kernel/IonescuTulcea/Traj
• mathlib4 Module Mathlib/RingTheory/Noetherian/Defs
• mathlib4 Module Mathlib/RingTheory/Noetherian/Filter
• mathlib4 Module Mathlib/RingTheory/Spectrum/Prime/Basic
• mathlib4 Module Mathlib/RingTheory/PicardGroup
• mathlib4 Module Mathlib/RingTheory/DividedPowers/Basic
• mathlib4 Module Mathlib/RingTheory/DividedPowers/DPMorphism
• mathlib4 Module Mathlib/Topology/Algebra/UniformConvergence
• mathlib4 Module Mathlib/Analysis/InnerProductSpace/Dual
• mathlib4 Module Mathlib/Topology/Algebra/Module/StrongTopology
• mathlib4 Module Mathlib/Analysis/InnerProductSpace/LinearPMap
• mathlib4 Module Mathlib/Topology/Algebra/Module/UniformConvergence
• mathlib4 Module Mathlib/Analysis/InnerProductSpace/OfNorm
• mathlib4 Module Mathlib/Topology/Algebra/Module/LinearPMap
• mathlib4 Module Mathlib/Analysis/Normed/Order/Lattice
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/FiniteExtension
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/InvariantExtension
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/IsPowMulFaithful
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/RingSeminorm
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/SeminormFromConst
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm
• mathlib4 Module Mathlib/Analysis/Normed/Unbundled/SpectralNorm
• mathlib4 Module Mathlib/Analysis/Real/Pi/Chudnovsky
• mathlib4 Module Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation
• mathlib4 Module Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order
• mathlib4 Module Mathlib/CategoryTheory/Adhesive
• mathlib4 Module Mathlib/CategoryTheory/Limits/VanKampen
• mathlib4 Module Mathlib/CategoryTheory/Elements
• mathlib4 Module Mathlib/CategoryTheory/Bicategory/Kan/Adjunction
• mathlib4 Module Mathlib/CategoryTheory/Monad/Algebra
• mathlib4 Module Mathlib/CategoryTheory/Monad/Kleisli
• mathlib4 Module Mathlib/CategoryTheory/Extensive
• mathlib4 Module Mathlib/CategoryTheory/Distributive/Cartesian
• mathlib4 Module Mathlib/CategoryTheory/Abelian/Basic
• mathlib4 Module Mathlib/CategoryTheory/Abelian/FreydMitchell
• mathlib4 Module Mathlib/CategoryTheory/Comma/Final
• mathlib4 Module Mathlib/CategoryTheory/Comma/Presheaf/Basic
• mathlib4 Module Mathlib/CategoryTheory/Comma/StructuredArrow/Final
• mathlib4 Module Mathlib/CategoryTheory/Filtered/CostructuredArrow
• mathlib4 Module Mathlib/CategoryTheory/Filtered/Final
• mathlib4 Module Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/Category
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/Equalizers
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/FilteredColimits
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/IndObject
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/ParallelPair
• mathlib4 Module Mathlib/CategoryTheory/Limits/Indization/Products
• mathlib4 Module Mathlib/CategoryTheory/Limits/Preserves/Presheaf
• mathlib4 Module Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives
• mathlib4 Module Mathlib/CategoryTheory/SmallObject/Basic

This page was built for software: mathlib