inv_prod

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.inv_prod

English

The inverse distributes over Cartesian product: (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) neg_prod]
theorem inv_prod [Inv β] (s : Set α) (t : Set β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru