mapRingHom_apply — Mathlib

English

For any f: K →+* L and x ∈ 𝓞 K, the L-component of mapRingHom f applied to x equals f applied to the K-component of x.

Русский

Для любого f: K →+* L и x ∈ 𝓞K, L-компонента mapRingHom f применённого к x равна f от K-компоненты x.

LaTeX

$$$(\\mathrm{mapRingHom}\, f\, x : L) = f(x)$$$

Lean4

@[simp]
theorem mapRingHom_apply {K L : Type*} [Field K] [Field L] (f : K →+* L) (x : 𝓞 K) : (mapRingHom f x : L) = f (x : K) :=
  rfl

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