mul_zero_eq_const

Mathlib.Algebra.GroupWithZero.Basic

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

English

x*0 is identically 0.

Русский

Левая точка умножения на ноль даёт ноль.

LaTeX

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

Lean4

/-- To match `mul_one_eq_id`. -/
theorem mul_zero_eq_const : (· * (0 : M₀)) = Function.const _ 0 :=
  funext mul_zero

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

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

Разделы

Аффилиация

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