OAI/Combinatorics/SumProduct/Alignment/SquareInduction08.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SquareInduction.compact_estimate_of_normalized line 33
2. theorem OAI.SquareInduction.quadratic_rank_statement line 97
3. theorem OAI.SquareInduction.quadratic_general_compact_producer line 131
4. theorem OAI.SquareInduction.quadratic_general_compact_all_lengths line 165
5. theorem OAI.SquareInduction.quadratic_general_metric_producer line 256