OAI/Topology/ArtinGroups/Geometry/Form.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.Geometric.FiniteOrbit.form line 14
2. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_symm line 17
3. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_sub_right line 23
4. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_smul_right line 27
5. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_neg_left line 31
6. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_invariant line 39
7. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_pos line 49
8. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_sum_left line 59
9. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_smul_left line 64
10. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_basis_row line 69
11. def OAI.HarmonicArtin.Geometric.FiniteOrbit.scale line 83
12. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.scale_pos line 85
13. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.scale_balance line 97
14. lemma OAI.HarmonicArtin.Geometric.FiniteOrbit.form_matrix line 106
15. theorem OAI.HarmonicArtin.Geometric.FiniteOrbit.principal_posDef line 120