instStarRingReal

Mathlib.Data.Real.Star

URI: https://scilib.ai/kg/mathlib#instStarRingReal

English

The real numbers form a star-ring with the trivial star operation, i.e., a* = a for all a ∈ ℝ.

Русский

Действительные числа образуют star-кольцо с тривиальной операцией звезды, то есть a* = a для всех a.

LaTeX

$$$a^* = a \\\\text{ for all } a \\in \\mathbb{R}$$$

Lean4

/-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/
instance : StarRing ℝ :=
  starRingOfComm

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

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

Разделы

Аффилиация

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