instFintypeSymbolsRing — Mathlib

English

The language of rings has five symbols; the corresponding type Language.ring.Symbols is finite with five elements.

Русский

Язык колец содержит пять символов; соответствующий тип Language.ring.Symbols конечен и имеет пять элементов.

LaTeX

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

Lean4

instance : Fintype Language.ring.Symbols :=
  ⟨⟨Multiset.ofList [Sum.inl ⟨2, .add⟩, Sum.inl ⟨2, .mul⟩, Sum.inl ⟨1, .neg⟩, Sum.inl ⟨0, .zero⟩, Sum.inl ⟨0, .one⟩], by
      dsimp [Language.Symbols]; decide⟩,
    by
    intro x
    dsimp [Language.Symbols]
    rcases x with ⟨_, f⟩ | ⟨_, f⟩
    · cases f <;> decide
    · cases f⟩

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