equivShrink_smul — Mathlib

English

EquivShrink respects scalar action: equivShrink α (m • x) = m • equivShrink α x.

Русский

EquivShrink сохраняет действие скаляра: equivShrink α (m • x) = m • equivShrink α x.

LaTeX

$$$\operatorname{equivShrink} \alpha (m \cdot x) = m \cdot \operatorname{equivShrink} \alpha x$$$

Lean4

@[simp]
theorem equivShrink_smul {M : Type*} [SMul M α] (m : M) (x : α) : equivShrink α (m • x) = m • equivShrink α x := by
  simp [Equiv.smul_def]

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