algebra_rat_subsingleton — Mathlib

English

There is at most one ℚ-algebra structure on any Ring R; the Subsingleton instance asserts uniqueness of the ℚ-algebra structure on R.

Русский

Для любой кольцевой структуры R существует по крайней мере одна ℚ-алгебра; Subsingleton утверждает уникальность структуры ℚ-алгебры на R.

LaTeX

$$$$ \\text{Subsingleton}(\\mathrm{Algebra}(\\mathbb{Q}, R)) $$$$

Lean4

instance algebra_rat_subsingleton {R} [Semiring R] : Subsingleton (Algebra ℚ R) :=
  ⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

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