English
There is a MonoidHom from S.leftInv to S sending each a ∈ S.leftInv to its right inverse in S, i.e., a ↦ S.fromLeftInv a, with the usual monoid-hom properties.
Русский
Существует моноидом-гомоморфизм из S.leftInv в S, отправляющий каждый элемент a ∈ S.leftInv его правый обратный в S, то есть a ↦ S.fromLeftInv a, сохраняющий единицу и умножение.
LaTeX
$$$ S.fromLeftInv : S.leftInv \\to* S $$$
Lean4
/-- The `MonoidHom` from `S.leftInv` to `S` sending an element to its right inverse in `S`. -/
@[to_additive (attr := simps) /-- The `AddMonoidHom` from `S.leftNeg` to `S` sending an element to
its right additive inverse in `S`. -/
]
noncomputable def fromCommLeftInv : S.leftInv →* S
where
toFun := S.fromLeftInv
map_one' := S.fromLeftInv_one
map_mul' x
y :=
Subtype.ext <| by
rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ← mul_assoc (x : M),
mul_fromLeftInv, one_mul, mul_fromLeftInv]
