Lean

swMATH15148MaRDI QIDQ27041FDOQ27041

Author name not available (Why is that?)

Source code repository: https://github.com/leanprover/lean

Described by source

• Formalizing double groupoids and cross modules in the Lean theorem prover
• The Lean theorem prover (system description)

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

• Formal Proof of Inverse function theorem
• Formal Proof of Stone–Weierstrass theorem
• Formal Proof of Wedderburn's little theorem
• Formal Proof of Open mapping theorem (functional analysis)
• Formal Proof of Kneser's addition theorem (combinatorics)
• Formal Proof of Erdős–Szekeres theorem
• Formal Proof of Open mapping theorem (complex analysis)
• Formal Proof of Gershgorin circle theorem
• Formal Proof of Lax–Milgram theorem
• mathlib4 Module Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass
• mathlib4 Module Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass
• mathlib4 Module Mathlib/AlgebraicTopology/ExtraDegeneracy
• mathlib4 Module Mathlib/AlgebraicTopology/DoldKan/Equivalence
• mathlib4 Module Mathlib/AlgebraicTopology/DoldKan/Homotopies
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/Basic
• mathlib4 Module Mathlib/AlgebraicTopology/SimplicialSet/Nerve
• mathlib4 Module Mathlib/AlgebraicTopology/SimplicialNerve
• mathlib4 Module Mathlib/AlgebraicTopology/DoldKan/Equivalence
• mathlib4 Module Mathlib/AlgebraicTopology/DoldKan/Homotopies
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/Basic
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/Cylinder
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/Homotopy
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/PathObject
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy
• mathlib4 Module Mathlib/AlgebraicTopology/ModelCategory/JoyalTrick
• mathlib4 Module Mathlib/AlgebraicTopology/SimplicialObject/II
• mathlib4 Module Mathlib/CategoryTheory/SmallObject/Basic
• mathlib4 Module Mathlib/CategoryTheory/Localization/CalculusOfFractions
• mathlib4 Module Mathlib/CategoryTheory/Localization/Construction
• mathlib4 Module Mathlib/Analysis/Seminorm
• mathlib4 Module Mathlib/Analysis/Convex/Gauge
• mathlib4 Module Mathlib/Analysis/LocallyConvex/Basic
• mathlib4 Module Mathlib/Analysis/LocallyConvex/Polar
• mathlib4 Module Mathlib/Analysis/Normed/Group/Seminorm
• mathlib4 Module Mathlib/Analysis/Calculus/Rademacher
• mathlib4 Module Mathlib/Topology/Algebra/Module/WeakBilin
• mathlib4 Module Mathlib/Topology/Algebra/Module/WeakDual
• mathlib4 Module Mathlib/MeasureTheory/Covering/Differentiation
• mathlib4 Module Mathlib/Analysis/Convex/Exposed
• mathlib4 Module Mathlib/MeasureTheory/Covering/VitaliFamily
• mathlib4 Module Mathlib/Analysis/Convex/Extreme
• mathlib4 Module Mathlib/MeasureTheory/Measure/Hausdorff
• mathlib4 Module Mathlib/Analysis/Convex/Intrinsic
• mathlib4 Module Mathlib/Analysis/Convex/KreinMilman
• mathlib4 Module Mathlib/Analysis/Convex/TotallyBounded
• mathlib4 Module Mathlib/Analysis/InnerProductSpace/Positive
• mathlib4 Module Mathlib/Analysis/LocallyConvex/BalancedCoreHull
• mathlib4 Module Mathlib/Analysis/LocallyConvex/Barrelled
• mathlib4 Module Mathlib/Analysis/LocallyConvex/Bounded
• mathlib4 Module Mathlib/Analysis/LocallyConvex/ContinuousOfBounded
• mathlib4 Module Mathlib/Analysis/LocallyConvex/StrongTopology
• mathlib4 Module Mathlib/Analysis/LocallyConvex/WeakDual
• 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
• mathlib4 Module Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu
• mathlib4 Module Mathlib/CategoryTheory/Bicategory/Coherence
• mathlib4 Module Mathlib/CategoryTheory/Monoidal/Free/Coherence

This page was built for software: Lean