toNormSMulClass_op — Mathlib

English

The NormSMulClass structure for the opposite ring extends to the scalar action of MulOpposite α on α, i.e., NormSMulClass (MulOpposite α) α holds with norm_smul a b = norm_mul b a.unop.

Русский

Структура NormSMulClass на противоположном кольце распространяется на скалярное умножение MulOpposite α на α: NormSMulClass (MulOpposite α) α, причём norm_smul a b = norm_mul b a.unop.

LaTeX

$$$NormSMulClass\\left( MulOpposite\\;\\alpha \\right)\\;\\alpha$$$

Lean4

instance (priority := 100) toNormSMulClass_op [SeminormedRing α] [NormMulClass α] : NormSMulClass αᵐᵒᵖ α where
  norm_smul a b := mul_comm ‖b‖ ‖a‖ ▸ norm_mul b a.unop

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