Lattice.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Integer arithmetic for the classical seven-color triangular lattice.

def OAI.Problem160.SevenLattice.normSq line 11
Source documentation
Squared Euclidean norm in a triangular lattice of unit spacing.
```
def normSq (a b : ℤ) : ℤ := a ^ 2 + a * b + b ^ 2
```
def OAI.Problem160.SevenLattice.color line 14
Source documentation
The index-seven coloring of triangular-lattice sites.
```
def color (a b : ℤ) : ZMod 7 := (a : ZMod 7) + 3 * (b : ZMod 7)
```
lemma OAI.Problem160.SevenLattice.normSq_nonneg line 16
lemma OAI.Problem160.SevenLattice.normSq_pos line 20
lemma OAI.Problem160.SevenLattice.seven_dvd_normSq line 28
lemma OAI.Problem160.SevenLattice.normSq_ge_seven line 35
lemma OAI.Problem160.SevenLattice.color_eq_iff_dvd line 39
lemma OAI.Problem160.SevenLattice.same_color_separation line 49
def OAI.Problem160.SevenLattice.colorFin line 58
Source documentation
The colors can be used directly as the Fin 7 target of a coloring.
```
def colorFin (a b : ℤ) : Fin 7 := color a b
```
Mentions: OAI.Problem160.SevenLattice.color
lemma OAI.Problem160.SevenLattice.colorFin_injective_value line 60