OAI/NumberTheory/Ostmann/Characters/SourceTemplateIndices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceHalfSize line 12
  2. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.roleListPositionEquiv_get line 15
  3. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.cellCoordinateEquiv line 23
  4. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.cellCoordinateEquiv_anchor line 29
  5. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.cellCoordinateEquiv_list line 36
  6. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.halfSourceCoordinateEquiv line 48
  7. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.halfRoleIndexEquiv line 52
  8. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceDoubleIndexEquiv line 56
  9. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceIndexEquiv line 60
  10. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceIndexEquiv_word_true line 66
  11. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceIndexEquiv_word_false line 73