to_continuousSMul_op — Mathlib

English

The action of M^op on M is continuous; i.e., the multiplication in the opposite setting defines a continuous SMul.

Русский

Действие M^op на M непрерывно; то есть умножение в противоположной обстановке задаёт непрерывное действие.

LaTeX

$$$\text{ContinuousSMul}(M^{\mathrm{op}}, M)$$$

Lean4

@[to_additive]
instance to_continuousSMul_op : ContinuousSMul Mᵐᵒᵖ M :=
  ⟨show Continuous ((fun p : M × M => p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id) from
      continuous_mul.comp <| continuous_swap.comp <| Continuous.prodMap MulOpposite.continuous_unop continuous_id⟩

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