OAI/RingTheory/FormalGroup/Correction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first coordinate correction and its nonzero cyclic residue class.

  1. def OAI.LowerCoefficientIntegration.firstCorrection line 15
  2. theorem OAI.LowerCoefficientIntegration.order_p_correction_and_residue_class line 19