Mathlib

Since 2021 I have been contributing to Mathlib3 / Mathlib4. Some of the more significant contributions are listed below.

• Order
  • Scott Continuity
  • Complete Partial Orders
• Topologies on a Preorder
  • Lower and Upper Topology
  • Upper and Lower Set Topology
  • Scott Topology
  • Lawson Topology
  • Hull-Kernel Topology
• Functional Analysis
  • L-summands
  • Bipolar Theorem
  • Banach Lattices
• Algebra
  • Jordan Algebras
  • Special Jordan Algebras
  • The centroid
  • Centroid of a *-ring
  • Lattice Ordered Groups
  • Basis expansion of a quadratic map
  • My work on non-associative structures was given a shout out by Jireh Loreaux during the Operator algebras talk at Lean Together 2024.
• Significant refactors
• The Strong Dual
  • 28726
  • 27699
• split Analysis/Convex/Normed into smaller files
• Unify concepts of Scott Topology
• Sesquilinear Forms to Sesquilinear Maps
  • 14988
  • 12547
  • 12132
  • 12124
  • 12122
  • 12078
  • 11280
  • 11278
  • 11097
• Quadratic Forms to Quadratic Maps
  • 7569
• Non-unital, non-associative algebras
  • 13089
  • 12924
  • 12938
• All Mathlib PRs
• Mathlib4
• Mathlib3