isBoundedSMulOpposite — Mathlib

English

For NonUnitalSeminormedRing α, right multiplication is a bounded scalar action on αᵐᵒᵖ by α, i.e., IsBoundedSMul αᵐᵒᵖ α.

Русский

Для NonUnitalSeminormedRing α, правое умножение ограничено как действие на αᵐᵒᵖ на α.

LaTeX

$$$IsBoundedSMul\\;\\left(\\text{MulOpposite } \\alpha\\right)\\;\\alpha$$$

Lean4

/-- Right multiplication is bounded. -/
instance isBoundedSMulOpposite [NonUnitalSeminormedRing α] : IsBoundedSMul αᵐᵒᵖ α
    where
  dist_smul_pair' x y₁ y₂ := by simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop
  dist_pair_smul' x₁ x₂ y := by simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop

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