fromLeftInv — Mathlib

English

There is a function fromLeftInv: S.leftInv → S that sends a left inverse to its right inverse in S.

Русский

Существует отображение fromLeftInv: S.leftInv → S, переводящее левый обратный элемент в правый обратный элемент в S.

LaTeX

$$fromLeftInv : S.leftInv → S$$

Lean4

/-- The function from `S.leftInv` to `S` sending an element to its right inverse in `S`.
This is a `MonoidHom` when `M` is commutative. -/
@[to_additive /-- The function from `S.leftAdd` to `S` sending an element to its right additive
    inverse in `S`. This is an `AddMonoidHom` when `M` is commutative. -/
    ]
noncomputable def fromLeftInv : S.leftInv → S := fun x ↦ x.prop.choose

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