card_ring

Mathlib.ModelTheory.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Ring.card_ring

English

The ring language has exactly five symbols.

Русский

Язык кольца имеет ровно пять символов.

LaTeX

$$$$ |\text{Language.ring}| = 5. $$$$

Lean4

@[simp]
theorem card_ring : card Language.ring = 5 :=
  by
  have : Fintype.card Language.ring.Symbols = 5 := rfl
  simp [Language.card, this]

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

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

Разделы

Аффилиация

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