OAI/NumberTheory/DukePrimeDegree/Geometry/NextProductRegularity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local finiteness of the intrinsic product on the next subgroup

  1. theorem OAI.DukePrimeDegree.InitialRootStep.ae_nextIntrinsicProduct_locallyFinite line 13