OAI/NumberTheory/Ostmann/QuadraticCenter/SquareKernelIndex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Square-root counts from a cyclic subgroup of small index

  1. def OAI.Ostmann.cosetSquareInjection line 12
  2. theorem OAI.Ostmann.cosetSquareInjection_injective line 24
  3. theorem OAI.Ostmann.square_kernel_card_le_two_index line 35

    Source documentation

    Each quotient class contains at most two square roots of one when the subgroup is cyclic. This will supply the factor four at powers of two.

    theorem square_kernel_card_le_two_index {G : Type*} [CommGroup G] [Fintype G]
    (H : Subgroup G) [IsCyclic H] :
    Nat.card {x : G // x ^ 2 = 1} ≤ 2 * Nat.card (G ⧸ H) := by
…