OAI/NumberTheory/Ostmann/Characters/SourceTemplateRoleIndices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.HalfRoleConstituent line 11
2. abbrev OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.HalfSourceCoordinates line 14
3. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.pairBoolSumEquiv line 17
4. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.anchorCoordinateEquiv line 25
5. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.anchorCoordinate line 28
6. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.halfRoleToCoordinates line 31
7. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.coordinatesToHalfRole line 38
8. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.halfRoleCoordinateEquiv line 47
9. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.constituentHalfEquiv line 77