card_units

Mathlib.Data.Fintype.Units

URI: https://scilib.ai/kg/mathlib#Fintype.card_units

← MathLib Explorer

English

If a ≠ b in α, then the subtype { c ∈ α | c = a ∨ c = b } has cardinality 2.

Русский

Если a ≠ b в α, то подтип { c ∈ α | c = a ∨ c = b } имеет кардинал 2.

LaTeX

$$$$|\\{ c : α \\mid c = a \\lor c = b \\}| = 2.$$$$

Lean4

theorem card_units [GroupWithZero α] [Fintype α] [DecidableEq α] : Fintype.card αˣ = Fintype.card α - 1 := by
  rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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