Model.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.EilenbergGanea.SourceGroup line 17
Also declared: ComparatorChallenges/EilenbergGanea.lean:92 (same declaration text).
def OAI.EilenbergGanea.cohomologicalDimension line 20
Source documentation
Integral, left-module cohomological dimension; no rational replacement.
Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:95 (different declaration text). Qualify references as OAI.EilenbergGanea.cohomologicalDimension@path.
```
def cohomologicalDimension (G : Type*) [Group G] : WithBot ℕ∞ :=
…
```
def OAI.EilenbergGanea.HasClassifyingSpace line 28
Source documentation
Ordinary K(G,1) of dimension at most n. The cell and space types have no finiteness or countability restriction. The contractible surjective covering is the usual universal-cover characterization of a classifying space.
Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:103 (different declaration text). Qualify references as OAI.EilenbergGanea.HasClassifyingSpace@path.
```
def HasClassifyingSpace (G : Type*) [Group G] (n : ℕ) : Prop :=
…
```
theorem OAI.EilenbergGanea.source_finitely_generated line 42
Source documentation
The finite-generation conjunct for the exact source height kernel.
```
theorem source_finitely_generated : Group.FG SourceGroup :=
…
```
Mentions: OAI.EilenbergGanea.SourceGroup
theorem OAI.EilenbergGanea.source_residuallyFinite line 51
Source documentation
The second exact conjunct of the source main theorem.
```
theorem source_residuallyFinite : Group.ResiduallyFinite SourceGroup := by
…
```
Mentions: OAI.EilenbergGanea.SourceGroup