mathlib

Cited in

(only showing first 100 items - show all)

Leveraging the information contained in theory presentations
Schemes in Lean
ProofWidgets
A Coq formalization of Lebesgue integration of nonnegative functions
Formalizing geometric algebra in Lean
KANT/KASH
Kenzo
MathJax
Agda
Coquelicot
Metamath
lens
McBits
HoTT
MathScheme
Lean
UniMath
AUTO2
HOLCF
Algebraic Numbers
Echelon Form
Density Compiler
Lp spaces
Perron Frobenius
Free Groups
Cytoscape.js
Mathematical Components
Stacks Project
TGView3D
Quaternions
Tog
Zeta_3_Irrational
Program logic for higher-order probabilistic programs in Isabelle/HOL
Metric spaces are paracompact
Combinatorics_Words
A bi-directional extensible interface between Lean and Mathematica
Formalizing Galois theory
Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
mizar-items
finmap
PCM library
Cubical Agda
mathlib4 Module Archive/MiuLanguage/Basic
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

This page was built for software: mathlib