smul_zero

Mathlib.RingTheory.OreLocalization.Basic

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

← MathLib Explorer

English

smul_zero: x • 0 = 0 for all x in the Ore localization.

Русский

smul_zero: x • 0 = 0 для всех x в локализации Оре.

LaTeX

$$$x \cdot 0 = 0$$$

Lean4

protected theorem smul_zero (x : R[S⁻¹]) : x • (0 : X[S⁻¹]) = 0 :=
  by
  induction x with
  | _ r s
  rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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