OAI/Combinatorics/SumProduct/Alignment/SquareInduction05.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RationalTailCoordinates.strict_filtration_refinement_geometry line 32
2. def OAI.SquareInduction.QuadraticCharacterData line 105
3. def OAI.SquareInduction.QuadraticCompactEstimate line 111
4. def OAI.SquareInduction.QuadraticNormalizedEstimate line 119
5. lemma OAI.SquareInduction.QuadraticCharacterData.mono line 128
6. def OAI.SquareInduction.QuadraticRankStatement line 140
7. theorem OAI.SquareInduction.quadratic_vertical_factor_alternative line 189
8. theorem OAI.SquareInduction.quadratic_source_factor_alternative line 272