coe_algebraMap_valuationSubring_eq

English

The two canonical ways of mapping an element from K0 to L0 via K preserve the same value, i.e., the algebra maps commute on the valuation subrings.

Русский

Две канонические схожие отображения элемента из K0 в L0 через K сохраняют одно и то же значение; отображения согласованы.

LaTeX

$$$\\operatorname{algebraMap}_{K_0,L_0}(x) = \\operatorname{algebraMap}_{K,L}(x)\\quad (x \\in K_0)$$$

Lean4

@[simp]
theorem coe_algebraMap_valuationSubring_eq (x : K₀) : (algebraMap K₀ L₀ x : L) = algebraMap K L (x : K) :=
  rfl

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