isUnit_of_mul_isUnit_left — Mathlib

English

In a commutative monoid, if a product x·y is a unit, then x is a unit.

Русский

В коммутативном моноиде, если произведение x·y является единицей, то x является единицей.

LaTeX

$$$\forall M [CommMonoid\ M] \forall x,y\in M:\ IsUnit(x\cdot y) \Rightarrow IsUnit(x)$$$

Lean4

@[to_additive]
theorem isUnit_of_mul_isUnit_left [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit x :=
  let ⟨z, hz⟩ := isUnit_iff_exists_inv.1 hu
  isUnit_iff_exists_inv.2 ⟨y * z, by rwa [← mul_assoc]⟩

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