OAI/NumberTheory/DukePrimeDegree/Geometry/ExtremalConjugationEntries.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conjugation acts by elementary row shears on the remaining root group

  1. lemma OAI.DukePrimeDegree.conjugation_entry_of_standard_column line 13