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 : M ≃* N) : Prime p ↔ Prime (e p)

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

theorem Prime.pow_dvd_of_dvd_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {a : M} {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} [CancelCommMonoidWithZero M] {p : M} {a : M} {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} [CancelCommMonoidWithZero M] {p : M} {a : M} {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_3} [CancelCommMonoidWithZero M] {p : M} {x : M} {y : M} (h : Prime p) {i : ℕ} (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ x ∨ p ∣ y

theorem not_irreducible_pow {M : Type u_3} [Monoid M] {x : M} {n : ℕ} (hn : n ≠ 1) : ¬Irreducible (x ^ n)

theorem Irreducible.of_map {M : Type u_1} {N : Type u_2} {F : Type u_3} [Monoid M] [Monoid N] [FunLike F M N] [MonoidHomClass F M N] {f : F} [IsLocalHom f] {x : M} (hfx : Irreducible (f x)) : Irreducible x

theorem irreducible_units_mul {M : Type u_1} [Monoid M] (a : Mˣ) (b : M) : Irreducible (↑a * b) ↔ Irreducible b

theorem irreducible_isUnit_mul {M : Type u_1} [Monoid M] {a : M} {b : M} (h : IsUnit a) : Irreducible (a * b) ↔ Irreducible b

theorem irreducible_mul_units {M : Type u_1} [Monoid M] (a : Mˣ) (b : M) : Irreducible (b * ↑a) ↔ Irreducible b

theorem irreducible_mul_isUnit {M : Type u_1} [Monoid M] {a : M} {b : M} (h : IsUnit a) : Irreducible (b * a) ↔ Irreducible b

theorem irreducible_mul_iff {M : Type u_1} [Monoid M] {a : M} {b : M} : Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

theorem Irreducible.map {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {F : Type u_3} [EquivLike F M N] [MulEquivClass F M N] (f : F) {x : M} (h : Irreducible x) : Irreducible (f x)

Irreducibility is preserved by multiplicative equivalences. Note that surjective + local hom is not enough. Consider the additive monoids M = ℕ ⊕ ℕ, N = ℕ, with a surjective local (additive) hom f : M →+ N sending (m, n) to 2m + n. It is local because the only add unit in N is 0, with preimage {(0, 0)} also an add unit. Then x = (1, 0) is irreducible in M, but f x = 2 = 1 + 1 is not irreducible in N.

theorem MulEquiv.irreducible_iff {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {F : Type u_3} [EquivLike F M N] [MulEquivClass F M N] (f : F) {a : M} : Irreducible (f a) ↔ Irreducible a

theorem Irreducible.not_square {M : Type u_1} [CommMonoid M] {a : M} (ha : Irreducible a) : ¬IsSquare a

theorem IsSquare.not_irreducible {M : Type u_1} [CommMonoid M] {a : M} (ha : IsSquare a) : ¬Irreducible a

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {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_square {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) : ¬IsSquare p

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

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

theorem DvdNotUnit.isUnit_of_irreducible_right {M : Type u_1} [CommMonoidWithZero M] {p : M} {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 : M} {q : M} (hp : ¬IsUnit p) (h : DvdNotUnit p q) : ¬Irreducible q

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

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

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

@[deprecated pow_injective_of_not_isUnit]

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

Alias of pow_injective_of_not_isUnit.

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