equivShrink_symm_smul — Mathlib

English

EquivShrink respects scalar multiplication: (equivShrink α)^{-1}(m • x) = m • (equivShrink α)^{-1} x for m acting on Shrink α.

Русский

EquivShrink сохраняет действие масштаба: (equivShrink α)^{-1}(m • x) = m • (equivShrink α)^{-1} x.

LaTeX

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

Lean4

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

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