OAI/NumberTheory/DukePrimeDegree/Geometry/PhysicalLeafInduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual remaining-group leaf-product induction step

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_basedLeaf_eq_intrinsic_of_next line 21