leftInv_le_isUnit — Mathlib

English

Let M be a commutative monoid and S a submonoid. Then every element of S.leftInv is a unit of M; i.e., S.leftInv ⊆ IsUnit.submonoid M.

Русский

Пусть M — коммутативный моноид и S — подпмонойд. Тогда каждый элемент S.leftInv является единицей M; то есть S.leftInv ⊆ IsUnit.submonoid M.

LaTeX

$$$ S.leftInv \\le IsUnit.submonoid M $$$

Lean4

@[to_additive]
theorem leftInv_le_isUnit : S.leftInv ≤ IsUnit.submonoid M := fun x ⟨y, hx⟩ ↦ ⟨⟨x, y, hx, mul_comm x y ▸ hx⟩, rfl⟩

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