inv_zero

Mathlib.Algebra.GroupWithZero.Pointwise.Finset

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

English

The inverse of the empty Finset is the empty Finset: (0)⁻¹ = 0.

Русский

Обратная пустого Finset равна пустому Finset: (0)⁻¹ = 0.

LaTeX

$$$0^{-1} = 0$$$

Lean4

@[simp]
protected theorem inv_zero : (0 : Finset α)⁻¹ = 0 := by ext; simp

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

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

Разделы

Аффилиация

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