OAI/RingTheory/DirectFiniteness/GluedGroup.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.GluedGroup.Generator line 15
  2. abbrev OAI.KaplanskyCounterexample.GluedGroup.LocalGenerator line 18

    Source documentation

    Generators belonging to a prescribed local point group.

    abbrev LocalGenerator (v : V) := {g : Generator (F := F) ℓ // v ∈ Inc g.1}

    Mentions: OAI.KaplanskyCounterexample.GluedGroup.Generator

  3. abbrev OAI.KaplanskyCounterexample.GluedGroup.PointGroup line 20
  4. def OAI.KaplanskyCounterexample.GluedGroup.localEvaluation line 24
  5. def OAI.KaplanskyCounterexample.GluedGroup.includeLocal line 28
  6. def OAI.KaplanskyCounterexample.GluedGroup.relators line 31
  7. abbrev OAI.KaplanskyCounterexample.GluedGroup.N line 35
  8. def OAI.KaplanskyCounterexample.GluedGroup.fromLocal line 37
  9. lemma OAI.KaplanskyCounterexample.GluedGroup.local_kernel_le line 40
  10. def OAI.KaplanskyCounterexample.GluedGroup.CoversPoints line 46

    Source documentation

    The direction partition covers every nonzero element of each point group.

    def CoversPoints : Prop := ∀ (v : V) (a : Fin 2 → ZMod ℓ), a ≠ 0 →
…
  11. lemma OAI.KaplanskyCounterexample.GluedGroup.localEvaluation_surjective line 49
  12. def OAI.KaplanskyCounterexample.GluedGroup.theta line 59
  13. lemma OAI.KaplanskyCounterexample.GluedGroup.theta_localEvaluation line 64
  14. lemma OAI.KaplanskyCounterexample.GluedGroup.theta_generator line 70
  15. instance OAI.KaplanskyCounterexample.GluedGroup.(instance at line 77) line 77
  16. def OAI.KaplanskyCounterexample.GluedGroup.EmbeddingClaim line 80