equivShrink_div — Mathlib

English

EquivShrink preserves division: equivShrink α (x / y) = equivShrink α x / equivShrink α y.

Русский

EquivShrink сохраняет деление: equivShrink α (x / y) = equivShrink α x / equivShrink α y.

LaTeX

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

Lean4

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

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