Basic.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite signed words, computable word problem, simple embeddings, and action-envelope predicates.

abbrev OAI.FiniteAlgebraicEnvelopes.Word line 14
Source documentation
Finite signed words, with true denoting a generator and false its inverse.
Distinct definitions of this name: ComparatorChallenges/BooneHigman.lean:9 (different declaration text). Qualify references as OAI.FiniteAlgebraicEnvelopes.Word@path.
```
abbrev Word (n : ℕ) := List (Fin n × Bool)
```
def OAI.FiniteAlgebraicEnvelopes.evalWord line 17
Source documentation
Evaluation in the specified finite generating family.
Distinct definitions of this name: ComparatorChallenges/BooneHigman.lean:11 (different declaration text). Qualify references as OAI.FiniteAlgebraicEnvelopes.evalWord@path.
```
def evalWord {G : Type u} [Group G] {n : ℕ} (s : Fin n → G) (w : Word n) : G :=
…
```
def OAI.FiniteAlgebraicEnvelopes.HasDecidableWordProblem line 21
Source documentation
Algorithmic decidability, not merely classical DecidablePred.
Distinct definitions of this name: ComparatorChallenges/BooneHigman.lean:16 (different declaration text). Qualify references as OAI.FiniteAlgebraicEnvelopes.HasDecidableWordProblem@path.
```
def HasDecidableWordProblem (G : Type u) [Group G] : Prop :=
…
```
def OAI.FiniteAlgebraicEnvelopes.EmbedsInFinitelyPresentedSimpleGroup line 27
Source documentation
The nontriviality in IsSimpleGroup is part of Mathlib's definition.
Distinct definitions of this name: ComparatorChallenges/BooneHigman.lean:21 (different declaration text). Qualify references as OAI.FiniteAlgebraicEnvelopes.EmbedsInFinitelyPresentedSimpleGroup@path.
```
def EmbedsInFinitelyPresentedSimpleGroup (G : Type u) [Group G] : Prop :=
…
```
def OAI.FiniteAlgebraicEnvelopes.HasActionEnvelope line 33
Source documentation
Action-envelope hypotheses.
```
def HasActionEnvelope (G : Type u) [Group G] : Prop :=
…
```