inv_product — Mathlib

English

The inverse of a pointwise product equals the pointwise product of inverses: (s ×ˢ t)^{-1} = s^{-1} ×ˢ t^{-1}.

Русский

Обратное к точечному произведению равняется точечному произведению обратных: (s ×ˢ t)^{-1} = s^{-1} ×ˢ t^{-1}.

LaTeX

$$$ (s \timesˢ t)^{-1} = s^{-1} \timesˢ t^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_product [DecidableEq β] [InvolutiveInv β] (s : Finset α) (t : Finset β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ :=
  mod_cast s.toSet.inv_prod t.toSet

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