OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListNextDegree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal fork transformation preserves the ordinary degree bound, isolated centers, and degree-one active ports.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.next_degreeBounds line 13