instSMulNat — Mathlib

English

The natural-number scalars act on ArchimedeanClass R by mapping n • mk x to mk(x^n).

Русский

Натуральные скаляры действуют на ArchimedeanClass R так: n • mk x = mk(x^n).

LaTeX

$$$$ n \cdot \operatorname{mk}(x) = \operatorname{mk}(x^n). $$$$

Lean4

instance : SMul ℕ (ArchimedeanClass R) where
  smul
    n :=
    lift (fun x ↦ mk (x ^ n)) fun x y h ↦ by
      induction n with
      | zero => simp
      | succ n IH => simp_rw [pow_succ, mk_mul, IH, h]

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