Square-free elements of unique factorization monoids

Main results:

• squarefree_mul_iff: x * y is square-free iff x and y have no common factors and are themselves square-free.

theorem squarefree_iff {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} (hx₀ : x ≠ 0) (hxu : ¬IsUnit x) : Squarefree x ↔ ∀ (p : R), Prime p → ¬p * p ∣ x

theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} {y : R} {p : R} {k : ℕ} (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ y

theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} {y : R} {p : R} {k : ℕ} (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ x

theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} {d : R} (hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y

theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} {d : R} (hy : Squarefree y) (h : d * d ∣ x * y) : d ∣ x

theorem squarefree_mul_iff {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} : Squarefree (x * y) ↔ (∀ (d : R), d ∣ x → d ∣ y → IsUnit d) ∧ Squarefree x ∧ Squarefree y

theorem exists_squarefree_dvd_pow_of_ne_zero {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} (hx : x ≠ 0) : ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n