OAI/NumberTheory/Ostmann/Arithmetic/SplitSquareSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

From the actual split relation to its reduced square equation

  1. theorem OAI.Ostmann.split_relation_gcd_eq line 14
  2. theorem OAI.Ostmann.split_relation_common_gcd line 19
  3. theorem OAI.Ostmann.split_relation_divide_gcd line 24
  4. theorem OAI.Ostmann.reduced_split_coefficients_coprime line 37
  5. theorem OAI.Ostmann.unit_coefficient_equation_iff line 45
  6. theorem OAI.Ostmann.unit_coefficient_gcd_eq line 52
  7. theorem OAI.Ostmann.unit_coefficient_reduce line 58
  8. theorem OAI.Ostmann.split_relation_iff_square line 78

    Source documentation

    The parent product is already exposed. The child product remains the uniform variable, and the split relation specifies its square.

    theorem split_relation_iff_square {G : Type*} [CommGroup G]
    (A B P x : G) : A * (P / x) = B * x ↔ x ^ 2 = A * P / B := by
…
  9. def OAI.Ostmann.splitSquareTarget line 95
  10. theorem OAI.Ostmann.unit_split_iff_square line 103