mul_iff — Mathlib

English

In a commutative monoid, IsUnit(xy) holds exactly when both IsUnit x and IsUnit y hold.

Русский

В коммутативном моноиде IsUnit(xy) эквивалентно IsUnit(x) и IsUnit(y).

LaTeX

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

Lean4

@[to_additive (attr := simp, grind =)]
theorem mul_iff [CommMonoid M] {x y : M} : IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y :=
  ⟨fun h => ⟨isUnit_of_mul_isUnit_left h, isUnit_of_mul_isUnit_right h⟩, fun h => IsUnit.mul h.1 h.2⟩

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