OAI/Algebra/Divisor/Normalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ControlledBoundary.FormalDivisor.positivePart line 11
2. def OAI.ControlledBoundary.FormalDivisor.negativePart line 14
3. lemma OAI.ControlledBoundary.FormalDivisor.positivePart_nonneg line 17
4. lemma OAI.ControlledBoundary.FormalDivisor.negativePart_nonneg line 20
5. lemma OAI.ControlledBoundary.FormalDivisor.signed_decomposition line 23
6. lemma OAI.ControlledBoundary.FormalDivisor.positivePart_coeff_lt_one line 32
7. lemma OAI.ControlledBoundary.FormalDivisor.negativePart_support_subset line 39
8. lemma OAI.ControlledBoundary.FormalDivisor.negativePart_signed_support line 48
9. theorem OAI.ControlledBoundary.FormalDivisor.normalize_correction line 63