Mathlib.Algebra.Group.Irreducible.Lemmas

not_irreducible_pow theorem

: ∀ {n : ℕ}, n ≠ 1 → ¬Irreducible (x ^ n)

Full source

@[to_additive]
lemma not_irreducible_pow : ∀ {n : ℕ}, n ≠ 1 → ¬ Irreducible (x ^ n)
  | 0, _ => by simp
  | n + 2, _ => by
    intro ⟨h₁, h₂⟩
    have := h₂ (pow_succ _ _)
    rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this
    exact h₁ (this.pow _)

Powers with exponent not equal to one are not irreducible

Informal description

For any natural number $n \neq 1$, the element $x^n$ is not irreducible in the monoid $M$.

irreducible_units_mul theorem

(u : Mˣ) : Irreducible (u * y) ↔ Irreducible y

Full source

@[to_additive]
lemma irreducible_units_mul (u : Mˣ) : IrreducibleIrreducible (u * y) ↔ Irreducible y := by
  simp only [irreducible_iff, Units.isUnit_units_mul, and_congr_right_iff]
  refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
  · rw [← u.isUnit_units_mul]
    apply h
    rw [mul_assoc, ← HAB]
  · rw [← u⁻¹.isUnit_units_mul]
    apply h
    rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]

Irreducibility of Left Multiplication by a Unit

Informal description

For any unit $u$ in a monoid $M$ and any element $y \in M$, the product $u \cdot y$ is irreducible if and only if $y$ is irreducible.

irreducible_isUnit_mul theorem

(h : IsUnit x) : Irreducible (x * y) ↔ Irreducible y

Full source

@[to_additive]
lemma irreducible_isUnit_mul (h : IsUnit x) : IrreducibleIrreducible (x * y) ↔ Irreducible y :=
  let ⟨x, ha⟩ := h
  ha ▸ irreducible_units_mul x

Irreducibility of Left Multiplication by a Unit Element

Informal description

For any element $x$ in a monoid $M$ that is a unit, and any element $y \in M$, the product $x \cdot y$ is irreducible if and only if $y$ is irreducible.

irreducible_mul_units theorem

(u : Mˣ) : Irreducible (y * u) ↔ Irreducible y

Full source

@[to_additive]
lemma irreducible_mul_units (u : Mˣ) : IrreducibleIrreducible (y * u) ↔ Irreducible y := by
  simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]
  refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
  · rw [← u.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB]
  · rw [← u⁻¹.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

Irreducibility of Product with Unit Element

Informal description

For any unit $u$ in a monoid $M$ and any element $y \in M$, the product $y \cdot u$ is irreducible if and only if $y$ is irreducible.

irreducible_mul_isUnit theorem

(h : IsUnit x) : Irreducible (y * x) ↔ Irreducible y

Full source

@[to_additive]
lemma irreducible_mul_isUnit (h : IsUnit x) : IrreducibleIrreducible (y * x) ↔ Irreducible y :=
  let ⟨x, hx⟩ := h
  hx ▸ irreducible_mul_units x

Irreducibility of Product with Unit Element (Right Multiplication)

Informal description

For any element $x$ in a monoid $M$ that is a unit, and any element $y \in M$, the product $y \cdot x$ is irreducible if and only if $y$ is irreducible.

irreducible_mul_iff theorem

: Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

Full source

@[to_additive]
lemma irreducible_mul_iff :
    IrreducibleIrreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x := by
  constructor
  · refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm
    · rwa [irreducible_mul_isUnit h'] at h
    · rwa [irreducible_isUnit_mul h'] at h
  · rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
    · rwa [irreducible_mul_isUnit hb]
    · rwa [irreducible_isUnit_mul ha]

Irreducibility of Product in a Monoid

Informal description

For any elements $x$ and $y$ in a monoid $M$, the product $x \cdot y$ is irreducible if and only if either: 1. $x$ is irreducible and $y$ is a unit, or 2. $y$ is irreducible and $x$ is a unit.

MulEquiv.irreducible_iff theorem

: Irreducible (f x) ↔ Irreducible x

Full source

@[to_additive]
lemma MulEquiv.irreducible_iff : IrreducibleIrreducible (f x) ↔ Irreducible x := by
  simp [_root_.irreducible_iff, (EquivLike.surjective f).forall, ← map_mul, -isUnit_map_iff]

Irreducibility is preserved under monoid isomorphism

Informal description

For any monoid isomorphism $f : M \to N$ and any element $x \in M$, the element $f(x)$ is irreducible in $N$ if and only if $x$ is irreducible in $M$.

Irreducible.of_map theorem

[FunLike F M N] [MonoidHomClass F M N] [IsLocalHom f] (hfx : Irreducible (f x)) : Irreducible x

Full source

lemma Irreducible.of_map [FunLike F M N] [MonoidHomClass F M N] [IsLocalHom f]
    (hfx : Irreducible (f x)) : Irreducible x where
  not_isUnit hu := hfx.not_isUnit <| hu.map f
  isUnit_or_isUnit := by
    rintro p q rfl; exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

Irreducibility is preserved under preimage by a local monoid homomorphism

Informal description

Let $M$ and $N$ be monoids, and let $f : M \to N$ be a monoid homomorphism that is a local homomorphism (i.e., preserves units in both directions). If $f(x)$ is an irreducible element in $N$, then $x$ is an irreducible element in $M$.

Irreducible.not_isSquare theorem

(ha : Irreducible x) : ¬IsSquare x

Full source

@[to_additive]
lemma Irreducible.not_isSquare (ha : Irreducible x) : ¬IsSquare x := by
  rw [isSquare_iff_exists_sq]
  rintro ⟨y, rfl⟩
  exact not_irreducible_pow (by decide) ha

Irreducible Elements Are Not Squares

Informal description

If an element $x$ in a monoid $M$ is irreducible, then $x$ is not a square, i.e., there does not exist an element $y \in M$ such that $x = y^2$.

IsSquare.not_irreducible theorem

(ha : IsSquare x) : ¬Irreducible x

Full source

@[to_additive]
lemma IsSquare.not_irreducible (ha : IsSquare x) : ¬Irreducible x := fun h => h.not_isSquare ha

Square Elements Are Not Irreducible

Informal description

If an element $x$ in a monoid $M$ is a square (i.e., there exists $y \in M$ such that $x = y^2$), then $x$ is not irreducible.