Formalized Mathematics

In this release I updated IsarMathLib to the new Isabelle 2025-1.

In this release I edited a theory file about actions of integers on abelian groups (-modules) contributed by Daniel de la Concepción Sáez a couple of years ago so that it is written in Isar dialect supported by the isarmathlib.org site and finished the pr…

This release is mostly about recent contributions by Daniel de la Concepción Sáez.

As in the title I updated IsarMathLib to Isabelle2025 released March 13th.

The discussion took place at the Hausdorff Center for Mathematics about a month ago.

Suppose is a pseudometric and consider the collection of relations on defined by . satisfies the following four conditions: This means that is a fundamental system of entourages and the supersets of (i.e. ) form a uniformity.

This release updates IsarMathLib to Isabelle2024.

This release adds definitions and basic facts about modules and vector spaces defined as ring (or field) actions on abelian groups.

A couple of years ago I got a task of writing a module for pricing gamma swaps.

Following the Isabelle2023 release I have released an updated version of IsarMathLib.