More lemmas about irreducible elements

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

theorem not_addIrreducible_nsmul {M : Type u_2} [AddMonoid M] {x : M} {n : ℕ} : n ≠ 1 → ¬AddIrreducible (n • x)

theorem irreducible_units_mul {M : Type u_2} [Monoid M] {y : M} (u : Mˣ) : Irreducible (↑u * y) ↔ Irreducible y

theorem addIrreducible_addUnits_add {M : Type u_2} [AddMonoid M] {y : M} (u : AddUnits M) : AddIrreducible (↑u + y) ↔ AddIrreducible y

theorem irreducible_isUnit_mul {M : Type u_2} [Monoid M] {x y : M} (h : IsUnit x) : Irreducible (x * y) ↔ Irreducible y

theorem addIrreducible_isAddUnit_add {M : Type u_2} [AddMonoid M] {x y : M} (h : IsAddUnit x) : AddIrreducible (x + y) ↔ AddIrreducible y

theorem irreducible_mul_units {M : Type u_2} [Monoid M] {y : M} (u : Mˣ) : Irreducible (y * ↑u) ↔ Irreducible y

theorem addIrreducible_add_addUnits {M : Type u_2} [AddMonoid M] {y : M} (u : AddUnits M) : AddIrreducible (y + ↑u) ↔ AddIrreducible y

theorem irreducible_mul_isUnit {M : Type u_2} [Monoid M] {x y : M} (h : IsUnit x) : Irreducible (y * x) ↔ Irreducible y

theorem addIrreducible_add_isAddUnit {M : Type u_2} [AddMonoid M] {x y : M} (h : IsAddUnit x) : AddIrreducible (y + x) ↔ AddIrreducible y

theorem irreducible_mul_iff {M : Type u_2} [Monoid M] {x y : M} : Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

theorem addIrreducible_add_iff {M : Type u_2} [AddMonoid M] {x y : M} : AddIrreducible (x + y) ↔ AddIrreducible x ∧ IsAddUnit y ∨ AddIrreducible y ∧ IsAddUnit x

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

theorem AddEquiv.addIrreducible_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [AddMonoid M] [AddMonoid N] {x : M} [EquivLike F M N] [AddEquivClass F M N] (f : F) : AddIrreducible (f x) ↔ AddIrreducible x

theorem Irreducible.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Monoid M] [Monoid N] {x : M} [EquivLike F M N] [MulEquivClass F M N] (f : F) : 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 x 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 AddIrreducible.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [AddMonoid M] [AddMonoid N] {x : M} [EquivLike F M N] [AddEquivClass F M N] (f : F) : AddIrreducible x → AddIrreducible (f x)

Irreducibility is preserved by additive equivalences.

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

theorem Irreducible.not_isSquare {M : Type u_2} [Monoid M] {x : M} (ha : Irreducible x) : ¬IsSquare x

theorem AddIrreducible.not_even {M : Type u_2} [AddMonoid M] {x : M} (ha : AddIrreducible x) : ¬Even x

theorem IsSquare.not_irreducible {M : Type u_2} [Monoid M] {x : M} (ha : IsSquare x) : ¬Irreducible x

theorem Even.not_addIrreducible {M : Type u_2} [AddMonoid M] {x : M} (ha : Even x) : ¬AddIrreducible x