Coprimality of the products a b (a + b) and a² + a b + b²

For coprime elements a and b of a commutative ring, the products a b (a + b) and a² + a b + b² are coprime. Modulo a, b and a + b the second product is b², a² and -a b, each of them coprime to the respective modulus.

Up to the factors 16, these products are the square root of the discriminant and the c₄ of the Frey–Hellegouarch curve y² = x (x - a) (x + b), whose discriminant is 16 (a b (a + b))² and whose c₄ is 16 (a² + a b + b²). So the coprimality says that away from 2 the Frey curve of a coprime pair has good or multiplicative reduction everywhere.

Main results

• IsCoprime.mul_mul_add_sq_add_mul_add_sq: if a and b are coprime, so are a b (a + b) and a² + a b + b².

theorem IsCoprime.mul_mul_add_sq_add_mul_add_sq {R : Type u_1} [CommRing R] {a b : R} (h : IsCoprime a b) : IsCoprime (a * b * (a + b)) (a ^ 2 + a * b + b ^ 2)

For coprime a and b, the products a b (a + b) and a² + a b + b² are coprime: modulo a, b and a + b the second is b², a² and -a b.