val_nnratCast — Mathlib

English

Let R be a field equipped with an involution. For every q in the nonnegative rationals Q_{\ge 0}, the embedding of q into the self-adjoint elements of R coincides with the embedding of q into R itself.

Русский

Пусть R — поле с инволюцией. Для каждого q из неотрицательных рациональных чисел Q_{\ge 0} отображение q в самосопряжённые элементы R совпадает с отображением q в R.

LaTeX

$$$ \\forall q \\in \\mathbb{Q}_{\\ge 0}, \\; (q : \\mathrm{selfAdjoint}(R)) = (q : R). $$$

Lean4

@[simp, norm_cast]
theorem val_nnratCast (q : ℚ≥0) : (q : selfAdjoint R) = (q : R) :=
  rfl

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