equivShrink_symm_div — Mathlib

English

Conjugation with division is preserved by the inverse shrink map: (equivShrink α)^{-1}(x / y) = (equivShrink α)^{-1} x / (equivShrink α)^{-1} y.

Русский

ОбратноеShrink-отображение сохраняет деление: (equivShrink α)^{-1}(x / y) = (equivShrink α)^{-1} x / (equivShrink α)^{-1} y.

LaTeX

$$$(\operatorname{equivShrink} \alpha)^{-1}(x / y) = (\operatorname{equivShrink} \alpha)^{-1} x / (\operatorname{equivShrink} \alpha)^{-1} y$$$

Lean4

@[to_additive (attr := simp)]
theorem equivShrink_symm_div [Div α] (x y : Shrink α) :
    (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y := by simp [Equiv.div_def]

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