instMonoidWithZeroHomClassReal — Mathlib

English

There is a structure-preserving map between InfinitePlace and the real numbers that is compatible with multiplication and zero.

Русский

Существуют отображения, сохраняющие структуру для бесконечного места и действительных чисел, сохраняющие умножение и ноль.

LaTeX

$$∀ {K} [Field K], MonoidWithZeroHomClass (NumberField.InfinitePlace K) K Real$$

Lean4

instance : MonoidWithZeroHomClass (InfinitePlace K) K ℝ
    where
  map_mul w _ _ := w.1.map_mul _ _
  map_one w := w.1.map_one
  map_zero w := w.1.map_zero

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