English
Let M be a monoid, a ∈ M, and u ∈ M×. Then a is a unit if and only if a·u is a unit; multiplying on the right by a unit does not change the unit-ness.
Русский
Пусть M — моноид, a ∈ M и u ∈ M×. Тогда a является единицей тогда и только тогда, когда a·u является единицей; умножение справа на единицу не изменяет свойство being единицы.
LaTeX
$$$\forall M [Monoid\ M] \forall a \in M \forall u \in M^{\times}: \ IsUnit(a\,u) \iff IsUnit(a)$$$
Lean4
/-- Multiplication by a `u : Mˣ` on the right doesn't affect `IsUnit`. -/
@[to_additive (attr := simp) /-- Addition of a `u : AddUnits M` on the right doesn't affect `IsAddUnit`. -/
]
theorem isUnit_mul_units [Monoid M] (a : M) (u : Mˣ) : IsUnit (a * u) ↔ IsUnit a :=
Iff.intro
(fun ⟨v, hv⟩ => by
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
rwa [mul_assoc, Units.mul_inv, mul_one] at this)
fun v => v.mul u.isUnit
