Basic.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EilenbergGanea.artinRelations line 14
Source documentation
The defining commutators of the right-angled Artin group.
Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:78 (different declaration text). Qualify references as OAI.EilenbergGanea.artinRelations@path.
```
def artinRelations {V : Type*} (L : SimpleGraph V) : Set (FreeGroup V) :=
…
```
abbrev OAI.EilenbergGanea.ArtinGroup line 18
Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:83 (different declaration text). Qualify references as OAI.EilenbergGanea.ArtinGroup@path.
def OAI.EilenbergGanea.height line 21
Source documentation
Every standard generator has integral height one.
Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:86 (different declaration text). Qualify references as OAI.EilenbergGanea.height@path.
```
def height {V : Type*} (L : SimpleGraph V) : ArtinGroup L →* Multiplicative ℤ :=
…
```
abbrev OAI.EilenbergGanea.artinGenerator line 35
theorem OAI.EilenbergGanea.height_generator line 37
theorem OAI.EilenbergGanea.adjacent_generators_commute line 41
def OAI.EilenbergGanea.edgeDifferences line 52
def OAI.EilenbergGanea.edgeGenerated line 55
theorem OAI.EilenbergGanea.edge_difference_mem line 57
theorem OAI.EilenbergGanea.reachable_difference_mem line 61
theorem OAI.EilenbergGanea.reachable_inv_difference_mem line 70

theorem OAI.EilenbergGanea.conjugate_mem_of_difference line 84

Source documentation

A group-theoretic conjugation identity used with edge differences.

theorem conjugate_mem_of_difference {A : Type*} [Group A] (K : Subgroup A)
    {g a e : A} (hga : g * a⁻¹ ∈ K) (he : e ∈ K) (ha : Commute a e) :
    g * e * g⁻¹ ∈ K := by
…

theorem OAI.EilenbergGanea.generator_conjugate_mem line 94
theorem OAI.EilenbergGanea.generator_inv_conjugate_mem line 105
theorem OAI.EilenbergGanea.edgeGenerated_normal line 121
theorem OAI.EilenbergGanea.edgeGenerated_eq_height_kernel line 134
Source documentation
For a connected defining graph, edge differences generate the full height kernel.
```
theorem edgeGenerated_eq_height_kernel (hconn : L.Preconnected) (v₀ : V) :
    edgeGenerated L = (height L).ker := by
…
```
Mentions: OAI.EilenbergGanea.edgeGenerated
theorem OAI.EilenbergGanea.height_kernel_fg line 158