English
If an element f belongs to a type F equipped with the MulSemiringActionHomClass data, then f can be regarded as an actual equivariant ring homomorphism from R to S twisted by φ, i.e., a concrete member of R →ₑ+*[φ] S.
Русский
Если элемент f принадлежит типу F, оборудованному данными MulSemiringActionHomClass, то f можно рассматривать как реальный эквивариантный кольцевой гомоморфизм R → S с twisting φ, то есть как конкретный элемент R →ₑ+*[φ] S.
LaTeX
$$$F \text{ satisfies } MulSemiringActionHomClass\; F\; φ\; R\; S \quad \Rightarrow \quad F \to (R \to_{\phi}^{\} S)$$$
Lean4
/-- Turn an element of a type `F` satisfying `MulSemiringActionHomClass F M R S` into an actual
`MulSemiringActionHom`. This is declared as the default coercion from `F` to
`MulSemiringActionHom M X Y`. -/
@[coe]
def _root_.MulSemiringActionHomClass.toMulSemiringActionHom [MulSemiringActionSemiHomClass F φ R S] (f : F) :
R →ₑ+*[φ] S :=
{ (f : R →+* S), (f : R →ₑ+[φ] S) with }
