instSMulNNRat — Mathlib

English

If R is a field with involution, the self-adjoint elements of R form a subfield under the inherited operations.

Русский

Если R — поле с инволюцией, то самосопряжённые элементы R образуют подполе в R под действием сохранённых операций.

LaTeX

$$$ \\{ x \\in R \\mid x^{*} = x \\} \\text{ is a subfield of } R. $$$

Lean4

instance instSMulNNRat : SMul ℚ≥0 (selfAdjoint R) where
  smul a x := ⟨a • (x : R), by rw [NNRat.smul_def]; exact .mul (.nnratCast a) x.prop⟩

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