instNonnegHomClassReal — Mathlib

English

There is a NonnegHomClass structure for FinitePlace K into Real, i.e., the associated evaluation maps take nonnegative values in an appropriate sense.

Русский

Существует структура NonnegHomClass для FinitePlace K в Real, то есть соответствующие отображения принимают неотрицательные значения.

LaTeX

$$$\\text{NonnegHomClass}(\\text{FinitePlace }K, K, \\mathbb{R})$$$

Lean4

instance : NonnegHomClass (FinitePlace K) K ℝ where apply_nonneg w := w.1.nonneg

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