English
The inverse of a bijective DistribMulActionHom is a DistribMulActionHom from B to A, obtained with a suitable inverse map g: B → A that is both a left and a right inverse of f.
Русский
Обратный биективному DistribMulActionHom имеется в виде DistribMulActionHom от B к A, получаемого через соответствующую обратную функцию g: B → A, являющуюся как левым, так и правым обратным к f.
LaTeX
$$$ \\exists g: B \\to A \\text{ such that } g \\circ f = \\mathrm{id}_A \\text{ and } f \\circ g = \\mathrm{id}_B \\;\\land\\; g \\text{ is DistribMulActionHom }$$$
Lean4
/-- `MulSemiringActionHomClass F M R S` states that `F` is a type of morphisms preserving
the ring structure and equivariant with respect to a `DistribMulAction`of `M` on `R` and `S` .
-/
abbrev MulSemiringActionHomClass (F : Type*) {M : outParam Type*} [Monoid M] (R S : outParam Type*) [Semiring R]
[Semiring S] [DistribMulAction M R] [DistribMulAction M S] [FunLike F R S] :=
MulSemiringActionSemiHomClass F (MonoidHom.id M) R S
