OAI/Combinatorics/SumProduct/Alignment/BracketHyperplanes02.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BracketHyperplanes.phase_finset_sum line 20
2. lemma OAI.BracketHyperplanes.character_linearOrbit line 27
3. theorem OAI.BracketHyperplanes.compact_bracket_linear_inverse line 46
4. lemma OAI.BracketHyperplanes.abs_dot_le line 80
5. theorem OAI.BracketHyperplanes.scaled_bracket_alternative line 95
6. lemma OAI.BracketDrift.dense_block line 239
7. theorem OAI.BracketDrift.relative_slope line 289