← all areas

Namespace Int 5 theorems

• Positive-definite binary form represents a squarefree integer ≥ 2 Int.exists_squarefree_sq_add_mul_add_mul_sq_of_sq_lt_four_mul 1 below · cited by 2 · depth 12
• Unimodular pairs mod n lift to coprime integer pairs Int.exists_modEq_and_modEq_and_isCoprime 0 below · cited by 6 · depth 13
• Normalising a quadratic translate: non-square, primitive, prime to p Int.exists_not_dvd_and_le_and_not_isSquare_and_forall_prime_of_sq_sub_four_mul_ne_zero 0 below · cited by 1 · depth 20
• A non-square positive value of k²-tk+n Int.exists_pos_and_not_isSquare_sq_sub_mul_add_of_sq_lt_four_mul 0 below · cited by 1 · depth 28
• Frobenius-fixed elements detect the exponent v modulo d Int.natCast_dvd_of_forall_frobeniusLift_pow_fixed_apply_zpow_eq 0 below · cited by 1 · depth 32