OAI/NumberTheory/DukePrimeDegree/Geometry/PhysicalIndependentBoxes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Independent rectangles with their actual quotient embeddings

The rectangle carries both its product conditional law and the geometric inclusions that identify its measure with an ambient restriction.

  1. theorem OAI.DukePrimeDegree.exists_remainingRoot_physical_independent_box line 17