OAI/Algebra/Finitistic/Encoding/AuxiliaryQuadraticPresentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.QuadraticPresentation.auxiliaryGroupAlgebra_hasFiniteQuadraticPresentation line 10

   Source documentation

   The Section 3 conversion applied to the exact Section 2 complex group algebra.

   theorem auxiliaryGroupAlgebra_hasFiniteQuadraticPresentation :
       HasFiniteQuadraticPresentation ℂ (MonoidAlgebra ℂ Presentation.AuxiliaryGroup) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation, OAI.LittleFinitistic.Presentation.AuxiliaryGroup

2. abbrev OAI.LittleFinitistic.QuadraticPresentation.AuxiliaryOldLetter line 14
3. abbrev OAI.LittleFinitistic.QuadraticPresentation.AuxiliaryOldEquation line 15
4. def OAI.LittleFinitistic.QuadraticPresentation.auxiliaryOriginalRelation line 18
5. def OAI.LittleFinitistic.QuadraticPresentation.auxiliaryWordBound line 22
6. theorem OAI.LittleFinitistic.QuadraticPresentation.auxiliaryWordBound_spec line 25
7. abbrev OAI.LittleFinitistic.QuadraticPresentation.AuxiliaryLetter line 30
8. abbrev OAI.LittleFinitistic.QuadraticPresentation.AuxiliaryEquation line 31
9. def OAI.LittleFinitistic.QuadraticPresentation.auxiliaryRelation line 33
10. instance OAI.LittleFinitistic.QuadraticPresentation.(instance at line 36) line 36
11. instance OAI.LittleFinitistic.QuadraticPresentation.(instance at line 37) line 37
12. theorem OAI.LittleFinitistic.QuadraticPresentation.auxiliaryRelation_degree line 40
13. def OAI.LittleFinitistic.QuadraticPresentation.auxiliaryQuadraticEquiv line 46

    Source documentation

    Concrete quadratic quotient and actual algebra equivalence, retaining the proved stable group's generators and relators and eliminating its word auxiliaries.

    def auxiliaryQuadraticEquiv : Original ℂ AuxiliaryLetter auxiliaryRelation ≃ₐ[ℂ]
        MonoidAlgebra ℂ Presentation.AuxiliaryGroup :=
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.Original, OAI.LittleFinitistic.QuadraticPresentation.AuxiliaryLetter, OAI.LittleFinitistic.QuadraticPresentation.auxiliaryRelation, OAI.LittleFinitistic.Presentation.AuxiliaryGroup