equivShrink_mul — Mathlib

English

EquivShrink is a monoid homomorphism: it preserves multiplication: equivShrink α (x · y) = equivShrink α x · equivShrink α y.

Русский

EquivShrink сохраняет умножение: equivShrink α (x · y) = equivShrink α x · equivShrink α y.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem equivShrink_mul [Mul α] (x y : α) : equivShrink α (x * y) = equivShrink α x * equivShrink α y := by
  simp [Equiv.mul_def]

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