instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom

English

There is a canonical coercion from any F satisfying MulSemiringActionHomClass to the concrete type R →ₑ+*[φ] S, giving a genuine equivariant additive ring homomorphism.

Русский

Существует каноническое приведение типа из любого F, удовлетворяющего MulSemiringActionHomClass, к реальному эквивариантному аддитивному кольцевому гомоморфизму R →ₑ+*[φ] S.

LaTeX

$$$F \text{ with } MulSemiringActionHomClass \Rightarrow F \to (R \to_{\phi}^{*} S)$$$

Lean4

/-- Any type satisfying `MulSemiringActionHomClass` can be cast into `MulSemiringActionHom` via
  `MulSemiringActionHomClass.toMulSemiringActionHom`. -/
instance [MulSemiringActionSemiHomClass F φ R S] : CoeTC F (R →ₑ+*[φ] S) :=
  ⟨MulSemiringActionHomClass.toMulSemiringActionHom⟩

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