OAI/NumberTheory/CubicMoment/Theta/CubicThetaCorePartition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth localization of the actual compact quotient core into the constructed arithmetic coordinate charts.

  1. lemma OAI.CubicFirstMoment.cubicThetaCore_smooth_partition line 13