OAI/GroupTheory/PolycyclicRecognition/Algebra/BooleanStepRing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The ring of integer-valued functions on finite Boolean partitions

Only finitely many of the chosen Boolean coordinates may be used by any one function. These functions form an actual subring, and each function has finite range. This provides the small coefficient algebra needed for a countable group.

  1. def OAI.PolycyclicRecognition.DependsOnBoolean line 17

    Source documentation

    A function is constant on the cells cut out by the indicated coordinates.

    def DependsOnBoolean (a : I → X → Bool) (s : Finset I) (f : X → ℤ) : Prop :=
…
  2. theorem OAI.PolycyclicRecognition.DependsOnBoolean.mono line 20
  3. def OAI.PolycyclicRecognition.booleanStepRing line 24
  4. theorem OAI.PolycyclicRecognition.booleanStepRing_coordinate line 46
  5. def OAI.PolycyclicRecognition.booleanPartitionCell line 53
  6. def OAI.PolycyclicRecognition.booleanPartitionPoint line 56
  7. instance OAI.PolycyclicRecognition.(instance at line 59) line 59
  8. def OAI.PolycyclicRecognition.booleanPartitionRepresentative line 63
  9. theorem OAI.PolycyclicRecognition.booleanPartitionPoint_representative line 66
  10. theorem OAI.PolycyclicRecognition.dependsOnBoolean_factorization line 72
  11. theorem OAI.PolycyclicRecognition.booleanStepRing_finite_range line 84