# More lemmas about irreducible elements #

source
theorem not_irreducible_pow {M : Type u_2} [Monoid M] {x : M} {n : ℕ} :
n ≠ 1 → ¬Irreducible (x ^ n)
source
theorem not_addIrreducible_nsmul {M : Type u_2} [AddMonoid M] {x : M} {n : ℕ} :
n ≠ 1 → ¬AddIrreducible (n • x)
source
theorem irreducible_units_mul {M : Type u_2} [Monoid M] {y : M} (u : M ˣ) :
Irreducible (↑u * y) ↔ Irreducible y
source
theorem addIrreducible_addUnits_add {M : Type u_2} [AddMonoid M] {y : M} (u : AddUnits M) :
AddIrreducible (↑u + y) ↔ AddIrreducible y
source
theorem irreducible_isUnit_mul {M : Type u_2} [Monoid M] {x y : M} (h : IsUnit x) :
Irreducible (x * y) ↔ Irreducible y
source
theorem addIrreducible_isAddUnit_add {M : Type u_2} [AddMonoid M] {x y : M} (h : IsAddUnit x) :
AddIrreducible (x + y) ↔ AddIrreducible y
source
theorem irreducible_mul_units {M : Type u_2} [Monoid M] {y : M} (u : M ˣ) :
Irreducible (y * ↑u) ↔ Irreducible y
source
theorem addIrreducible_add_addUnits {M : Type u_2} [AddMonoid M] {y : M} (u : AddUnits M) :
AddIrreducible (y + ↑u) ↔ AddIrreducible y
source
theorem irreducible_mul_isUnit {M : Type u_2} [Monoid M] {x y : M} (h : IsUnit x) :
Irreducible (y * x) ↔ Irreducible y
source
theorem addIrreducible_add_isAddUnit {M : Type u_2} [AddMonoid M] {x y : M} (h : IsAddUnit x) :
AddIrreducible (y + x) ↔ AddIrreducible y
source
theorem irreducible_mul_iff {M : Type u_2} [Monoid M] {x y : M} :
Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
source
theorem addIrreducible_add_iff {M : Type u_2} [AddMonoid M] {x y : M} :
AddIrreducible (x + y) ↔ AddIrreducible x ∧ IsAddUnit y ∨ AddIrreducible y ∧ IsAddUnit x
source
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
source
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
source
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`.

source
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.

source
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
source
theorem Irreducible.not_isSquare {M : Type u_2} [Monoid M] {x : M} (ha : Irreducible x) :
¬IsSquare x
source
theorem AddIrreducible.not_even {M : Type u_2} [AddMonoid M] {x : M} (ha : AddIrreducible x) :
¬Even x
source
theorem IsSquare.not_irreducible {M : Type u_2} [Monoid M] {x : M} (ha : IsSquare x) :
¬Irreducible x
source
theorem Even.not_addIrreducible {M : Type u_2} [AddMonoid M] {x : M} (ha : Even x) :
¬AddIrreducible x