deriv_zero_left

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.deriv_zero_left

English

For all a, deriv 0 a = a.

Русский

Для любого a произведная 0 действует как тождество: deriv 0 a = a.

LaTeX

$$$$ \operatorname{deriv} 0 a = a $$$$

Lean4

theorem deriv_zero_left (a) : deriv 0 a = a := by rw [deriv_zero, id_eq]

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

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

Разделы

Аффилиация

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