OAI/Algebra/GroupRing/RelationTorsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.RelationTorsion.fox_pow line 15
2. lemma OAI.TorsionFreeZeroDivisors.RelationTorsion.norm_zpowers line 21
3. theorem OAI.TorsionFreeZeroDivisors.RelationTorsion.torsion_free line 31

   Source documentation

   The translated integral relation-area identity rules out actual finite-order quotient elements, via the exact cyclic norm complex on free integral modules.

   theorem torsion_free
       (hz : ∀ts : List (Term (A:=A) (I:=I)),FreeGroup.mk (word rel ts)=1→total rel ts=0) :
   …