nsmulMemClass — Mathlib

English

There is a SMulMemClass S Nat M given an AddMonoid structure on M and AddSubmonoidClass on S.

Русский

Существует SMulMemClass S Nat M при наличии структуры AddMonoid на M и AddSubmonoidClass на S.

LaTeX

$$$\\text{SMulMemClass } S\\ Nat\\ M$$$

Lean4

/-- Not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`. -/
theorem nsmulMemClass {S M : Type*} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] : SMulMemClass S ℕ M where
  smul_mem n _x hx := nsmul_mem hx n

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