instAddCommMonoid — Mathlib

English

ArchimedeanClass R forms an additive monoid.

Русский

ArchimedeanClass R образует аддитивный моноид.

LaTeX

$$$$ \operatorname{mk}(x) + 0 = \operatorname{mk}(x). $$$$

Lean4

instance : AddCommMonoid (ArchimedeanClass R)
    where
  add_assoc := add_assoc'
  zero_add := zero_add'
  add_zero x := add_comm x _ ▸ zero_add' x
  nsmul n x := n • x
  nsmul_zero
    x := by
    induction x with
    | mk x => rw [← mk_pow, pow_zero, mk_one]
  nsmul_succ n
    x := by
    induction x with
    | mk x => rw [← mk_pow, pow_succ, mk_mul, mk_pow]

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