English
Let M be a monoid, u ∈ M×, a ∈ M. Multiplication on the left by a unit does not affect whether a is a unit: IsUnit(↑u × a) is equivalent to IsUnit a.
Русский
Пусть M — моноид, u ∈ M×, a ∈ M. Умножение слева на единицу не влияет на то, является ли элемент единицей: IsUnit(↑u × a) эквивалентно IsUnit a.
LaTeX
$$$\forall M [Monoid\ M] (u \in M^{\times}) (a \in M): IsUnit(↑u \cdot a) \iff IsUnit(a)$$$
Lean4
/-- Multiplication by a `u : Mˣ` on the left doesn't affect `IsUnit`. -/
@[to_additive (attr := simp) /-- Addition of a `u : AddUnits M` on the left doesn't affect `IsAddUnit`. -/
]
theorem isUnit_units_mul {M : Type*} [Monoid M] (u : Mˣ) (a : M) : IsUnit (↑u * a) ↔ IsUnit a :=
Iff.intro
(fun ⟨v, hv⟩ => by
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
rwa [← mul_assoc, Units.inv_mul, one_mul] at this)
u.isUnit.mul
