# Nonsingular systems of equations over arbitrary groups

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Kervaire theorem for groups](../../preprints/The-Kervaire-Theorem-for-Groups-September-24-2026/The-Kervaire-Theorem-for-Groups-September-24-2026.pdf)

## Scope

Kervaire's conjecture states that the free product of a nontrivial group with an infinite cyclic group cannot be normally generated by one element. The linked formalization proves the stronger coefficient-injectivity statement used in the paper: for any group $A$ and any relator in $A*\mathbb Z$ whose exponent sum in the cyclic generator is $1$ or $-1$, the natural map from $A$ into the quotient by that relator is injective. This is the selected unimodular-relator result underlying the conjecture.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Coefficient-group injectivity for unimodular one-relator quotients | [Kervaire.lean](../ComparatorChallenges/Kervaire.lean) |