coe_map

Mathlib.Algebra.Field.Subfield.Basic

URI: https://scilib.ai/kg/mathlib#Subfield.coe_map

English

The image of a subfield under a ring homomorphism f is a subfield of the codomain, and the underlying sets satisfy (s.map f : Set L) = f '' s.

Русский

Образ подполе под гомоморфизмом f является подполем области, и множества согласованы: (s.map f : Set L) = f '' s.

LaTeX

$$$ (s.map f : Set L) = f '' s $$$

Lean4

@[simp, norm_cast]
theorem coe_map : (s.map f : Set L) = f '' s :=
  rfl

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

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

Разделы

Аффилиация

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