zero_mul_eq_const

Mathlib.Algebra.GroupWithZero.Basic

URI: https://scilib.ai/kg/mathlib#zero_mul_eq_const

English

0*x is identically 0.

Русский

Нулевой множитель слева действует как ноль в любой аргумент.

LaTeX

$$For all x, 0 * x = 0$$

Lean4

/-- To match `one_mul_eq_id`. -/
theorem zero_mul_eq_const : ((0 : M₀) * ·) = Function.const _ 0 :=
  funext zero_mul

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

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

Разделы

Аффилиация

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