OAI/NumberTheory/Ostmann/Characters/AnchorOneSidedEdge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.changed_anchor_code_one_sided line 10
2. theorem OAI.Ostmann.signed_square_nonprincipal line 18
3. theorem OAI.Ostmann.changed_anchor_code_characters line 29

   Source documentation

   The first alternative uses the small anchor as the short modulus; the second uses the bulk prime as the short modulus and the big anchor as long.

   theorem changed_anchor_code_characters {p q : ℕ}
       (χanchor : DirichletCharacter ℂ p) (χbulk : DirichletCharacter ℂ q)
       (hanchor : χanchor ^ 2 ≠ 1) (hbulk : χbulk ^ 2 ≠ 1)
       (ε ε' c c' : ℤ) (hε : ε = 1 ∨ ε = -1) (hε' : ε' = 1 ∨ ε' = -1)
       (hc : c = 1 ∨ c = -1) (hc' : c' = 1 ∨ c' = -1) (hne : c ≠ c') :
       (χanchor ^ (ε * c - ε' * c') ≠ 1 ∧ ε - ε' = 0) ∨
         (ε * c - ε' * c' = 0 ∧ χbulk ^ (ε - ε') ≠ 1) := by
   …