instSMulCommClassSubtypeMem_2 — Mathlib

English

The second form of the commutativity result for the subtype under SMulMemClass assumptions.

Русский

Вторая форма результата коммутативности для подтипа при предпосылках SMulMemClass.

LaTeX

$$$\\forall s:\\; SMulCommClass N M α \\Rightarrow SMulCommClass N M (Subtype ...) $$$

Lean4

@[to_additive]
instance (priority := 50) [SMulCommClass N M α] : SMulCommClass N M s where
  smul_comm _ _ _ := Subtype.ext (smul_comm ..)

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