zero_mul

Mathlib.RingTheory.OreLocalization.Ring

URI: https://scilib.ai/kg/mathlib#OreLocalization.zero_mul

English

The deprecated lemma: 0 · x = 0.

Русский

Устаревшая лемма: 0 · x = 0.

LaTeX

$$0 \cdot x = 0$$

Lean4

@[deprecated zero_mul (since := "2025-08-20")]
protected theorem zero_mul (x : R[S⁻¹]) : 0 * x = 0 :=
  OreLocalization.zero_smul x

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

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

Разделы

Аффилиация

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