star_nnratCast — Mathlib

English

In a division semiring with a star, a nonnegative rational embedded into the ring is fixed by star.

Русский

В делимой полукольце с операцией звезды элемент nnrat, отображаемый как q, фиксируется звездой.

LaTeX

$$$\\\\star(q : R) = q \\\\quad (q \\\\in \\\\mathbb{Q}_{\\\\ge 0}).$$$

Lean4

@[simp, norm_cast]
theorem star_nnratCast [DivisionSemiring R] [StarRing R] (q : ℚ≥0) : star (q : R) = q :=
  (congr_arg unop <| map_nnratCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) q).trans (unop_nnratCast _)

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