map_one

Mathlib.Algebra.AddConstMap.Basic

URI: https://scilib.ai/kg/mathlib#AddConstMapClass.map_one

English

In the unit case, f(1) = f(0) + b.

Русский

В случае единицы выполняется f(1) = f(0) + b.

LaTeX

$$$\\forall f \\in F:\\ f(1) = f(0) + b$$$

Lean4

theorem map_one [AddZeroClass G] [One G] [Add H] [AddConstMapClass F G H 1 b] (f : F) : f 1 = f 0 + b :=
  map_const f

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

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

Разделы

Аффилиация

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