coe_map

Mathlib.RingTheory.NonUnitalSubring.Basic

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

English

The set in the codomain obtained as the image of s under f equals f '' s.

Русский

Множество образа подполья s под отображением f равно изображению f над s.

LaTeX

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

Lean4

@[simp]
theorem coe_map (f : F) (s : NonUnitalSubring R) : (s.map f : Set S) = f '' s :=
  rfl

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

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

Разделы

Аффилиация

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