OAI/Algebra/GroupRing/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.TorsionFree line 10

   Source documentation

   Ordinary group torsion-freeness, without requiring uniqueness of all roots.

   Also declared: ComparatorChallenges/TorsionFreeZeroDivisors.lean:8 (same declaration text).

   def TorsionFree (G : Type) [Group G] : Prop :=
   …

2. def OAI.TorsionFreeZeroDivisors.HasFiniteTwoDimensionalClassifyingSpace line 14

   Source documentation

   A connected finite Hausdorff 2-dimensional CW K(G,1).

   Also declared: ComparatorChallenges/TorsionFreeZeroDivisors.lean:12 (same declaration text).

   def HasFiniteTwoDimensionalClassifyingSpace (G : Type) [Group G] : Prop :=
   …

3. def OAI.TorsionFreeZeroDivisors.MainTheorem line 30

   Source documentation

   The entire main theorem, including its "Moreover" clause.

   Also declared: ComparatorChallenges/TorsionFreeZeroDivisors.lean:28 (same declaration text).

   def MainTheorem : Prop :=
   …