English
The inverse of the shrink equivalence respects multiplication: (equivShrink α)^{-1} (x · y) = (equivShrink α)^{-1} x · (equivShrink α)^{-1} y for x,y in Shrink α.
Русский
Обратное отображение shrink-эквивалентности сохраняет умножение: (equivShrink α)^{-1}(x·y) = (equivShrink α)^{-1}x · (equivShrink α)^{-1}y для x,y ∈ Shrink α.
LaTeX
$$$(\operatorname{equivShrink} \alpha)^{-1}(x \cdot y) = (\operatorname{equivShrink} \alpha)^{-1}x \cdot (\operatorname{equivShrink} \alpha)^{-1}y$$$
Lean4
@[to_additive (attr := simp)]
theorem equivShrink_symm_mul [Mul α] (x y : Shrink α) :
(equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y := by simp [Equiv.mul_def]
