equivShrink_symm_inv — Mathlib

English

Inverse shrink commutes with inversion: (equivShrink α)^{-1}(x^{-1}) = ((equivShrink α)^{-1} x)^{-1}.

Русский

Обратное shrink-коммутирует с обращением: (equivShrink α)^{-1}(x^{-1}) = ((equivShrink α)^{-1} x)^{-1}.

LaTeX

$$$\left(\operatorname{equivShrink} \alpha\right)^{-1}(x^{-1}) = \left((\operatorname{equivShrink} \alpha)^{-1} x\right)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem equivShrink_symm_inv [Inv α] (x : Shrink α) : (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹ := by
  simp [Equiv.inv_def]

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