English
Multiplication on the left by a unit does not affect irreducibility: for any unit u, Irreducible (u·y) is equivalent to Irreducible y.
Русский
Умножение слева на единицу не влияет на неразложимость: для любой единицы u имеет место равносильность Irreducible (u·y) ≡ Irreducible y.
LaTeX
$$$\\\\forall {M} [Monoid M] {y : M} (u : Units M), Irreducible (u \\cdot y) \\\\Leftrightarrow Irreducible y$$$
Lean4
@[to_additive]
theorem irreducible_units_mul (u : Mˣ) : Irreducible (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]
