mem_fieldRange_self

Mathlib.Algebra.Field.Subfield.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.mem_fieldRange_self

English

Let f: K →+* L be a field homomorphism. Then for every x ∈ K, f(x) lies in the range (fieldRange) of f.

Русский

Пусть f: K →+* L — гомоморфизм полей. Тогда для каждого x ∈ K выполняется f(x) ∈ fieldRange f.

LaTeX

$$$\forall x : K,\; f(x) \in f.fieldRange$$$

Lean4

theorem mem_fieldRange_self (x : K) : f x ∈ f.fieldRange :=
  exists_apply_eq_apply _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru