More lemmas about irreducible elements #
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))
:
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