instTrivialStarReal — Mathlib

English

The real numbers can be equipped with a star operation that acts as the identity on every element; i.e., x^* = x for all x ∈ ℝ.

Русский

Числа ℝ можно снабдить операцией звезды, которая является тождественной на всех элементах: для всех x ∈ ℝ выполняется x^* = x.

LaTeX

$$$\forall x \in \mathbb{R}, x^* = x$$$

Lean4

instance : TrivialStar ℝ :=
  ⟨fun _ => rfl⟩

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