nat_algebra_subsingleton — Mathlib

English

There exists at most one ℕ-algebra structure on any semiring R; i.e., the ℕ-algebra structure is unique.

Русский

Для произвольного полупрерывного кольца R существует не более одной структуры ℕ-алгебры; то есть структура ℕ-алгебры единственна.

LaTeX

$$$\operatorname{Subsingleton}(\mathrm{Algebra}\ \mathbb{N}\ R).$$$

Lean4

instance nat_algebra_subsingleton : Subsingleton (Algebra ℕ R) :=
  ⟨fun P Q => by ext; simp⟩

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