Associated, prime, and irreducible elements.

In this file we define the predicate Prime p saying that an element of a commutative monoid with zero is prime. Namely, Prime p means that p isn't zero, it isn't a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;

In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Irreducible, however this is not true in general.

We also define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient.

theorem comap_prime {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {F : Type u_3} {G : Type u_4} [FunLike F M N] [MonoidWithZeroHomClass F M N] [FunLike G N M] [MulHomClass G N M] (f : F) (g : G) {p : M} (hinv : ∀ (a : M), g (f a) = a) (hp : Prime (f p)) : Prime p

theorem MulEquiv.prime_iff {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {p : M} {E : Type u_5} [EquivLike E M N] [MulEquivClass E M N] (e : E) : Prime (e p) ↔ Prime p

theorem prime_units_mul {M : Type u_1} [CommMonoidWithZero M] {y : M} (u : Mˣ) : Prime (↑u * y) ↔ Prime y

theorem prime_isUnit_mul {M : Type u_1} [CommMonoidWithZero M] {x y : M} (h : IsUnit x) : Prime (x * y) ↔ Prime y

theorem prime_mul_units {M : Type u_1} [CommMonoidWithZero M] {y : M} (u : Mˣ) : Prime (y * ↑u) ↔ Prime y

theorem prime_mul_isUnit {M : Type u_1} [CommMonoidWithZero M] {x y : M} (h : IsUnit x) : Prime (y * x) ↔ Prime y

theorem Prime.left_dvd_or_dvd_right_of_dvd_mul {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : M} (hp : Prime p) {a b : M} : a ∣ p * b → p ∣ a ∨ a ∣ b

theorem Prime.pow_dvd_of_dvd_mul_left {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ a) (h' : p ^ n ∣ a * b) : p ^ n ∣ b

theorem Prime.pow_dvd_of_dvd_mul_right {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ b) (h' : p ^ n ∣ a * b) : p ^ n ∣ a

theorem Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M} {n : ℕ} (hp : Prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a

theorem prime_pow_succ_dvd_mul {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p x y : M} (h : Prime p) {i : ℕ} (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ x ∨ p ∣ y

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : M} (hp : Prime p) {a b : M} {k l : ℕ} : p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b

theorem Prime.not_isSquare {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : M} (hp : Prime p) : ¬IsSquare p

theorem IsSquare.not_prime {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {a : M} (ha : IsSquare a) : ¬Prime a

theorem not_prime_pow {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {a : M} {n : ℕ} (hn : n ≠ 1) : ¬Prime (a ^ n)

theorem DvdNotUnit.isUnit_of_irreducible_right {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) (hq : Irreducible q) : IsUnit p

theorem not_irreducible_of_not_unit_dvdNotUnit {M : Type u_1} [CommMonoidWithZero M] {p q : M} (hp : ¬IsUnit p) (h : DvdNotUnit p q) : ¬Irreducible q

theorem DvdNotUnit.not_unit {M : Type u_1} [CommMonoidWithZero M] {p q : M} (hp : DvdNotUnit p q) : ¬IsUnit q

theorem DvdNotUnit.ne {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p q : M} (h : DvdNotUnit p q) : p ≠ q

theorem pow_injective_of_not_isUnit {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) : Function.Injective fun (n : ℕ) => q ^ n

theorem pow_inj_of_not_isUnit {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) {m n : ℕ} : q ^ m = q ^ n ↔ m = n

theorem IsRelPrime.of_map {M : Type u_3} {N : Type u_4} {F : Type u_5} [Monoid M] [Monoid N] [FunLike F M N] [MulHomClass F M N] (f : F) [IsLocalHom f] {a b : M} (hab : IsRelPrime (f a) (f b)) : IsRelPrime a b