instMonoidWithZeroHomClassReal — Mathlib

English

There is a canonical MonoidWithZeroHomClass structure sending FinitePlace K to Real, i.e., the finite place data respects multiplication, identity, and zero, when viewed as a real-valued homomorphism.

Русский

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

LaTeX

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

Lean4

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

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