OAI/Algebra/GroupRing/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.main line 13

   Source documentation

   A torsion-free group with a finite 2-dimensional K(G,1) and zero divisors. Both zero-divisor factors are nonzero, and torsion-freeness is ordinary absence of all nontrivial finite-order elements.

   Distinct definitions of this name: ComparatorChallenges/TorsionFreeZeroDivisors.lean:35 (same statement text; different proof or body). Qualify references as OAI.TorsionFreeZeroDivisors.main@path.

   theorem main : MainTheorem := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MainTheorem