OAI/Algebra/GroupRing/ConcreteTorsion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ConcreteTorsion.signedLabels line 13
2. lemma OAI.TorsionFreeZeroDivisors.ConcreteTorsion.signedLabels_reverse line 15
3. lemma OAI.TorsionFreeZeroDivisors.ConcreteTorsion.freeLetter_eq line 19
4. lemma OAI.TorsionFreeZeroDivisors.ConcreteTorsion.letters_eq line 23
5. def OAI.TorsionFreeZeroDivisors.ConcreteTorsion.unsigned line 26
6. theorem OAI.TorsionFreeZeroDivisors.ConcreteTorsion.torsion_free line 45
7. theorem OAI.TorsionFreeZeroDivisors.torsion_free_finitely_presented_zero_divisors line 60

   Source documentation

   The exact group's ordinary torsion-freeness and both nonzero zero-divisor factors, proved without assuming a resolution or topological asphericity. The finite classifying-space clause remains separate and is not asserted here.

   theorem torsion_free_finitely_presented_zero_divisors :
       ∃ (G : Type) (inst : Group G), letI : Group G := inst
   …