mul — Mathlib

English

If a specializes to b in a topological monoid with continuous multiplication, then a^n specializes to b^n for any natural n.

Русский

Если a специализируется на b в топологической моноиде с непрерывным умножением, то a^n специализируется на b^n для любого натурального n.

LaTeX

$$$a \xrightarrow{\mathrm{Specializes}} b \Rightarrow \forall n \in \mathbb{N},\ a^n \xrightarrow{\mathrm{Specializes}} b^n$$$

Lean4

@[to_additive]
protected theorem mul {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) : (a * c) ⤳ (b * d) :=
  hab.smul hcd

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