OAI/Algebra/GroupRing/ConcreteModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.HasFiniteTwoDimensionalClassifyingSpace.of_equiv line 10
2. theorem OAI.TorsionFreeZeroDivisors.ConcreteModel.has_model line 29

   Source documentation

   The finite exact two-dimensional model of the actual sampled graph group. The cover contraction is built by absorbing physical disk-track obstructions through the proved integral cell-boundary splitting.

   theorem has_model : HasFiniteTwoDimensionalClassifyingSpace (ConcreteGroup.G rep r) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.HasFiniteTwoDimensionalClassifyingSpace, OAI.TorsionFreeZeroDivisors.ConcreteGroup.G