ncard_inv

Mathlib.Algebra.Group.Pointwise.Set.Card

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

English

For a set s in a group with involutive inverse, the ncard of s⁻¹ equals the ncard of s.

Русский

Для множества s в группе с инволютивной операцией ncard(s⁻¹) = ncard(s).

LaTeX

$$$$ s^{-1}.ncard = s.ncard $$$$

Lean4

@[to_additive (attr := simp)]
theorem ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard := by simp [ncard]

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

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

Разделы

Аффилиация

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