down_one

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.down_one

English

The down map sends the unit 1 in SetSemiring α to 1 in Set α.

Русский

Отображение down отправляет единицу 1 в SetSemiring α в 1 в Set α.

LaTeX

$$down(1) = 1$$

Lean4

@[simp]
theorem down_one : (1 : SetSemiring α).down = 1 :=
  rfl

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

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

Разделы

Аффилиация

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