OAI/RingTheory/DirectFiniteness/GroupEmbedding.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.GluedGroup.localEvaluation_word line 13
2. lemma OAI.KaplanskyCounterexample.GluedGroup.relators_allowed line 25
3. theorem OAI.KaplanskyCounterexample.GluedGroup.generator_ne_one line 43

   Source documentation

   No nonzero line generator collapses in the actual all-word presentation.

   theorem generator_ne_one (hInc : ∀ f, (Inc f).Nonempty)
       (hinj : ∀ v f, v ∈ Inc f → Function.Injective (totalMap Inc ℓ incMap v f))
       (hind : ∀ v f g, v ∈ Inc f → v ∈ Inc g → f ≠ g →
         ∀ a b, totalMap Inc ℓ incMap v f a + totalMap Inc ℓ incMap v g b = 0 → a = 0)
       (hgirth : 12 ≤ (Planar.incidenceGraph (fun v f => v ∈ Inc f)).egirth)
       (g : Generator (F := F) ℓ) :
   …

   Mentions: OAI.KaplanskyCounterexample.GluedGroup.totalMap, OAI.KaplanskyCounterexample.Planar.incidenceGraph, OAI.KaplanskyCounterexample.GluedGroup.Generator

4. theorem OAI.KaplanskyCounterexample.GluedGroup.theta_injective line 66