coe_eq — Mathlib

English

The coercion from ℚ_p to PadicAlgCl p is equal to the algebraMap embedding.

Русский

Встраивание ℚ_p в PadicAlgCl p совпадает с каноническим вложением через algebraMap.

LaTeX

$$$$ (\operatorname{Coe}\colon \mathbb{Q}_p \to \operatorname{PadicAlgCl}(p)) = \operatorname{algebraMap}_{\mathbb{Q}_p\to \operatorname{PadicAlgCl}(p)}. $$$$

Lean4

theorem coe_eq : (Coe.coe : ℚ_[p] → PadicAlgCl p) = algebraMap ℚ_[p] (PadicAlgCl p) :=
  rfl

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