isUnit_of_mul_isUnit_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem isUnit_of_mul_isUnit_right [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit y :=
  @isUnit_of_mul_isUnit_left _ _ y x <| by rwa [mul_comm]

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