OAI/Geometry/HeilbronnTriangle/DiagonalDetImage.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.DiagonalDetImage.diagonalThree line 14
  2. def OAI.Problem355.DiagonalDetImage.finalDiagonalUnit line 17
  3. theorem OAI.Problem355.DiagonalDetImage.finalDiagonalUnit_val line 21
  4. theorem OAI.Problem355.DiagonalDetImage.finalDiagonalUnit_det line 26
  5. theorem OAI.Problem355.DiagonalDetImage.finalDiagonalUnit_fixes line 31
  6. def OAI.Problem355.DiagonalDetImage.determinantValues line 42
  7. theorem OAI.Problem355.DiagonalDetImage.mem_determinantValues line 47
  8. theorem OAI.Problem355.DiagonalDetImage.card_determinantValues_lower line 51
  9. def OAI.Problem355.DiagonalDetImage.annihilatorEquivCongruenceUnits line 61
  10. theorem OAI.Problem355.DiagonalDetImage.isUnit_one_add_of_annihilates_prime_power line 77
  11. theorem OAI.Problem355.DiagonalDetImage.card_congruenceUnits_eq_annihilator line 101
  12. theorem OAI.Problem355.DiagonalDetImage.card_congruenceUnits_prime_power line 109
  13. theorem OAI.Problem355.DiagonalDetImage.determinantValues_zero line 118
  14. theorem OAI.Problem355.DiagonalDetImage.card_determinantValues_prime_power_zero line 124
  15. theorem OAI.Problem355.DiagonalDetImage.card_determinantValues_prime_power_lower line 134
  16. theorem OAI.Problem355.DiagonalDetImage.card_determinantValues_ratio line 141
  17. theorem OAI.Problem355.DiagonalDetImage.determinantValues_eq_stabilizer_map line 157
  18. theorem OAI.Problem355.DiagonalDetImage.determinant_mem_of_diagonal_form line 166
  19. theorem OAI.Problem355.DiagonalDetImage.card_stabilizer_det_image_ratio_of_diagonal_form line 197