opposite_mid — Mathlib

English

If M acts on N, and SMul M N and SMulCommClass M N N hold, then there is IsScalarTower M Nᵐᵒᵖ N with smul_assoc = mul_smul_comm.

Русский

Если M действует на N, и выполняются SMul M N и SMulCommClass M N N, то существует IsScalarTower M N^{op} N со свойством smul_assoc = mul_smul_comm.

LaTeX

$$$\text{instance opposite_mid } : IsScalarTower M N^{op} N$,\; smul\_assoc _ _ _ := mul\_smul\_comm _ _ _$$$

Lean4

@[to_additive]
instance opposite_mid {M N} [Mul N] [SMul M N] [SMulCommClass M N N] : IsScalarTower M Nᵐᵒᵖ N where
  smul_assoc _ _ _ := mul_smul_comm _ _ _

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