OAI/Geometry/HeilbronnTriangle/DiagonalStabilizer.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.DiagonalStabilizer.diagonal3 line 14
  2. abbrev OAI.Problem355.DiagonalStabilizer.Ann line 17
  3. abbrev OAI.Problem355.DiagonalStabilizer.FixingMatrices line 19
  4. lemma OAI.Problem355.DiagonalStabilizer.fixing_entry line 22
  5. lemma OAI.Problem355.DiagonalStabilizer.fixing_first_column line 29
  6. lemma OAI.Problem355.DiagonalStabilizer.fixing_other_column line 33
  7. def OAI.Problem355.DiagonalStabilizer.encode line 40
  8. lemma OAI.Problem355.DiagonalStabilizer.encode_injective line 47
  9. theorem OAI.Problem355.DiagonalStabilizer.card_fixingMatrices_le line 62
  10. abbrev OAI.Problem355.DiagonalStabilizer.FixingUnits line 67
  11. def OAI.Problem355.DiagonalStabilizer.forgetUnits line 70
  12. lemma OAI.Problem355.DiagonalStabilizer.forgetUnits_injective line 73
  13. theorem OAI.Problem355.DiagonalStabilizer.card_fixingUnits_diagonal_le line 80
  14. def OAI.Problem355.DiagonalStabilizer.conjugateFixing line 86
  15. lemma OAI.Problem355.DiagonalStabilizer.conjugateFixing_injective line 99
  16. theorem OAI.Problem355.DiagonalStabilizer.card_fixingUnits_of_diagonal_form_le line 109
  17. theorem OAI.Problem355.DiagonalStabilizer.card_stabilizer_of_diagonal_form_le line 118