Yamaguchi Lean 4 Library

YamaLean4Lib is Naganori Yamaguchi's Lean 4 library for formalized mathematics. It includes formalizations of profinite groups, Fox differentials, completed group algebras, the Reidemeister–Schreier theorem, and related topics.

7 libraries536 files8748 declarations

GitHub repository for the Lean source package.

Sort Order

Library

CompletedGroupAlgebra

10 top-level groups | 58 files | 743 declarations

This module formalizes completed group algebras as inverse limits over finite quotients.

Library

CrowellExactSequence

3 top-level groups | 18 files | 258 declarations

This module formalizes the Crowell--Blanchfield--Lyndon exact sequence and its completed version.

Library

FenchelNielsenZomorrodian

2 top-level groups | 76 files | 951 declarations | 2 axiom

This module formalizes the Fenchel--Nielsen--Zomorrodian theorem. It currently uses two explicit local axioms for the finite-subgroup frontier. Reference: arXiv:2605.02577.

Library

FoxDifferential

4 top-level groups | 204 files | 2884 declarations

This module formalizes Fox differentials and Fox coordinates for free and profinite groups.

Library

ProCGroups

23 top-level groups | 131 files | 2782 declarations

This module formalizes basic constructions for profinite and pro-\(C\) groups.

Library

ReidemeisterSchreier

7 top-level groups | 48 files | 1078 declarations

This module formalizes the Reidemeister--Schreier theorem.

Library

Yama2026_Sections_1_And_2_1

1 top-level groups | 1 files | 52 declarations

This module formalizes Section 1 and Subsection 2.1 of Yamaguchi's paper on center-freeness.