OAI/Topology/ArtinGroups/Geometry/InvariantForm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.Geometric.invariantForm line 14
  2. lemma OAI.HarmonicArtin.Geometric.invariantForm_symm line 17
  3. lemma OAI.HarmonicArtin.Geometric.invariantForm_sub_right line 23
  4. lemma OAI.HarmonicArtin.Geometric.invariantForm_smul_right line 27
  5. lemma OAI.HarmonicArtin.Geometric.invariantForm_neg_left line 31
  6. lemma OAI.HarmonicArtin.Geometric.invariantForm_invariant line 39
  7. lemma OAI.HarmonicArtin.Geometric.invariantForm_pos line 49
  8. lemma OAI.HarmonicArtin.Geometric.invariantForm_basis_row line 59
  9. def OAI.HarmonicArtin.Geometric.invariantScale line 73
  10. lemma OAI.HarmonicArtin.Geometric.invariantScale_pos line 75
  11. lemma OAI.HarmonicArtin.Geometric.invariantScale_balance line 82
  12. lemma OAI.HarmonicArtin.Geometric.invariantForm_matrix line 88
  13. theorem OAI.HarmonicArtin.Geometric.cartan_posDef line 113