irreducible_mul_units — Mathlib

English

Multiplication on the right by a unit preserves irreducibility: for any unit u, Irreducible (y·u) ↔ Irreducible y.

Русский

Умножение справа на единицу сохраняет неразложимость: Irreducible (y·u) ⇔ Irreducible y.

LaTeX

$$$\\\\forall {M} [Monoid M] {y : M} (u : Units M), Irreducible (y \\cdot u) \\\\Leftrightarrow Irreducible y$$$

Lean4

@[to_additive]
theorem irreducible_mul_units (u : Mˣ) : Irreducible (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]

Похожие утверждения