Version 1.31.0

uniform structure on an ordered loop valued pseudometric space

Version 1.30.0

• Modules: linear combinations, linear dependency, submodules, spans, Z-modules
• Update to Isabelle2024

Version 1.29.0

• New theory files on modules and vector spaces
• Ring_ZF_2 and Ring_ZF_3 edited for isarmathlib.org

Version 1.28.1

IsarMathLib has been updated for Isabelle2023.
Topology_ZF_8 and Group_ZF_5 added to isarmathlib.org.

Version 1.28.0

Added the binomial theorem for commutative rings.

Version 1.27.0

• Ring theory and Zariski topology: reaches the result that the spectrum of a quotient ring is homeomorphic to a closed subspace of the spectrum of the original ring .
• A new theory on Finite State Machines. Reaches a proof that non-deterministic finite state automata determine the same languages as deterministic finite state automata. Also includes results on operations closed for regular languages.

Version 1.26.0

1. Algebraic topology:

• Ring ideal definition
• Product and sum of ideals
• Prime ideal definition
• Maximal ideal definition
• Spectrum and Zariski topology
• Ring homomorphism
• Quotient of ring by ideal

Basics:

• Pascal's triangle

Version 1.25.0

Added a theorem that uniform spaces are regular, translated from Metamath, with dependencies, 29 new theorems total.

Version 1.24.0

• Updated to Isabelle2022
• Added some theorems about Hausdorff spaces and neighborhood systems

Version 1.23.0

The presentation layer tool got rewritten in F#. Added a theorem stating that an ordered loop valued metric space is T₂.