OAI/Algebra/GroupRing/ConeChains.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.ConeChains.Cells line 19
  2. abbrev OAI.TorsionFreeZeroDivisors.ConeChains.TwoChain line 20
  3. lemma OAI.TorsionFreeZeroDivisors.ConeChains.edge_reverse line 21
  4. lemma OAI.TorsionFreeZeroDivisors.ConeChains.representative_edge line 23
  5. lemma OAI.TorsionFreeZeroDivisors.ConeChains.letters_reverse line 25
  6. def OAI.TorsionFreeZeroDivisors.ConeChains.eval line 27
  7. lemma OAI.TorsionFreeZeroDivisors.ConeChains.eval_inverse line 31
  8. def OAI.TorsionFreeZeroDivisors.ConeChains.cell line 38

    Source documentation

    Actual oriented physical two-cell with its group translate. The translation is measured from the common cone apex, not from the endpoint of the edge.

    def cell (g : G) (d : D) : Cells Γ R label letters :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.ConeChains.Cells

  9. lemma OAI.TorsionFreeZeroDivisors.ConeChains.cell_reverse line 41
  10. def OAI.TorsionFreeZeroDivisors.ConeChains.charge line 51
  11. lemma OAI.TorsionFreeZeroDivisors.ConeChains.charge_reverse line 55
  12. def OAI.TorsionFreeZeroDivisors.ConeChains.coneCharge line 68
  13. lemma OAI.TorsionFreeZeroDivisors.ConeChains.coneCharge_reverse line 72
  14. theorem OAI.TorsionFreeZeroDivisors.ConeChains.chain_zero line 87

    Source documentation

    Sharp arrangement exclusion annihilates the genuine free integral physical-cell charge of every lifted cone boundary picture.

    theorem chain_zero
    (hex : ∀{P : Type}[Fintype P][Nonempty P]
      (b : SphericalPicture.Data (O:=P) Γ label inv),¬b.Reduced) :
…

    Mentions: OAI.TorsionFreeZeroDivisors.SphericalPicture.Data