OAI/NumberTheory/CubicGauss/Eisenstein.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Eisenstein integers, norm, residue quotients and cubic first-moment definitions.

  1. lemma OAI.CubicFirstMoment.residueRepresentative_spec line 15

    Also declared: OAI/NumberTheory/CubicGram/ResidueCharacters.lean:83 (same declaration text).

  2. lemma OAI.CubicFirstMoment.real_coordinates_norm line 19

    Also declared: OAI/NumberTheory/CubicGram/EuclideanDomain.lean:29 (same declaration text).

  3. lemma OAI.CubicFirstMoment.complex_coordinates line 27

    Also declared: OAI/NumberTheory/CubicGram/EuclideanDomain.lean:40 (same declaration text).