inv_insert

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inv_insert

English

The inverse distributes over insertion: (insert a s)⁻¹ = insert a⁻¹ s⁻¹.

Русский

Обратное распределяется через добавление: (insert a s)⁻¹ = insert a⁻¹ s⁻¹.

LaTeX

$$$ (\mathrm{insert}\ a\ s)^{-1} = \mathrm{insert}\ a^{-1}\ s^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_insert (a : α) (s : Finset α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹ :=
  image_insert _ _ _

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

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

Разделы

Аффилиация

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