zsmulMemClass — Mathlib

English

There is a SMulMemClass S Int M given a SubNegMonoid structure on M and AddSubmonoid-like conditions.

Русский

Существует SMulMemClass S Int M при наличии SubNegMonoid на M и аналогичных условий.

LaTeX

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

Lean4

/-- Not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`. -/
theorem zsmulMemClass {S M : Type*} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] : SMulMemClass S ℤ M where
  smul_mem n _x hx := zsmul_mem hx n

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