smulCommClass — Mathlib

English

Given an equivalence e: α ≃ β, if SMulCommClass M N β holds, then by transporting via e, SMulCommClass M N α also holds.

Русский

Пусть есть эквивалент e: α ≃ β, если SMulCommClass M N β, то через перенос по e получаем SMulCommClass M N α.

LaTeX

$$$\text{Equiv.smulCommClass } M N e: SMulCommClass M N α$ given $SMulCommClass M N β$.$$

Lean4

/-- Transfer `SMulCommClass` across an `Equiv` -/
@[to_additive /-- Transfer `VAddCommClass` across an `Equiv` -/
    ]
protected theorem smulCommClass (e : α ≃ β) [SMulCommClass M N β] :
    letI := e.smul M
    letI := e.smul N
    SMulCommClass M N α :=
  letI := e.smul M
  letI := e.smul N
  { smul_comm := by simp [smul_def, smul_comm] }

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