English
The real numbers can be endowed with a star-ordered ring structure in which the star map is the identity.
Русский
Числа ℝ можно наделить структурой звездоупорядоченного кольца, при этом операция звезды тождественна.
LaTeX
$$$\exists *: \mathbb{R} \to \mathbb{R},\ \forall x \in \mathbb{R}, x^{*} = x$$$
Lean4
/-- Although the instance `RCLike.toStarOrderedRing` exists, it is locked behind the
`ComplexOrder` scope because currently the order on `ℂ` is not enabled globally. But we
want `StarOrderedRing ℝ` to be available globally, so we include this instance separately.
In addition, providing this instance here makes it available earlier in the import
hierarchy; otherwise in order to access it we would need to import
`Mathlib/Analysis/RCLike/Basic.lean`. -/
instance instStarOrderedRing : StarOrderedRing ℝ :=
StarOrderedRing.of_nonneg_iff' add_le_add_left fun r =>
by
refine ⟨fun hr => ⟨√r, (mul_self_sqrt hr).symm⟩, ?_⟩
rintro ⟨s, rfl⟩
exact mul_self_nonneg s
