instSMulInt — Mathlib

English

There is an action of the integers on ArchimedeanClass(R) extending multiplication to negative and positive powers: if mk x = mk y, then mk (x^n) = mk (y^n) for all integers n.

Русский

Существует действие целых чисел на ArchimedeanClass(R), продолжающее умножение на степени: если mk(x) = mk(y), то mk(x^n) = mk(y^n) для всех целых n.

LaTeX

$$$\forall n \in \mathbb{Z},\ \operatorname{mk}(x) = \operatorname{mk}(y) \rightarrow \operatorname{mk}(x^{n}) = \operatorname{mk}(y^{n}).$$$

Lean4

instance : SMul ℤ (ArchimedeanClass R) where
  smul n := lift (fun x ↦ mk (x ^ n)) fun x y h ↦ by obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simp [h]

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