OAI/NumberTheory/DukePrimeDegree/Geometry/ExtremalRootQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The real quotient by the remaining roots

The extremal matrix entry is additive on its positive-root group. Its kernel is precisely the remaining root group. Thus the subgroup removed in the product induction is normal, as required by EK2003, Proposition 8.3.

  1. theorem OAI.DukePrimeDegree.neutral_root_entry_mul line 22
  2. def OAI.DukePrimeDegree.neutralRootEntryHom line 47
  3. theorem OAI.DukePrimeDegree.neutralRootEntryHom_ker line 65
  4. theorem OAI.DukePrimeDegree.remaining_roots_normal line 91