OAI/GroupTheory/ArtinCAT0/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArtinCAT0.Assembly.blockMain_zero line 8
2. lemma OAI.ArtinCAT0.Assembly.blockMain_one line 12
3. lemma OAI.ArtinCAT0.Assembly.blockMain_relations line 17
4. theorem OAI.ArtinCAT0.Assembly.not_geometric line 26

   Source documentation

   The literal 116-generator presentation has no geometric CAT(0) action.

   theorem not_geometric (X : Type u) [MetricSpace X] [ProperSpace X] [Nonempty X]
       [MulAction MainGroup X] : ¬GeometricAction MainGroup X := by
   …

   Mentions: OAI.ArtinCAT0.MainGroup

5. theorem OAI.ArtinCAT0.main line 53

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: And, OAI.ArtinCAT0.Letters, Eq, OAI.ArtinCAT0.Label, OAI.ArtinCAT0.explicitMatrix, OfNat.ofNat, Nat, Ne, Or, Top.top, MetricSpace, ProperSpace, Nonempty, MulAction, OAI.ArtinCAT0.ArtinGroup, OAI.ArtinCAT0.artinRelators, Not, OAI.ArtinCAT0.GeometricAction

   Proof uses: And.intro, OAI.ArtinCAT0.explicitMatrix_symmetric, OAI.ArtinCAT0.explicitMatrix_diagonal, OAI.ArtinCAT0.explicitMatrix_values, OAI.ArtinCAT0.Assembly.not_geometric

   28 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/ArtinCAT0.lean:65 (same statement text; different proof or body). Qualify references as OAI.ArtinCAT0.main@path.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.