zero_smul

Mathlib.RingTheory.OreLocalization.Ring

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

← MathLib Explorer

English

For any x in the Ore localization X[S^{-1}], 0 acts as zero: 0 • x = 0.

Русский

Для любого x в локализации X[S^{-1}] 0 действует как ноль: 0 • x = 0.

LaTeX

$$0 \cdot x = 0$$

Lean4

protected theorem zero_smul (x : X[S⁻¹]) : (0 : R[S⁻¹]) • x = 0 :=
  by
  induction x with
  | _ r s
  rw [OreLocalization.zero_def, oreDiv_smul_char 0 r 1 s 0 1 (by simp)]; simp

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

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

Разделы

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

Аффилиация

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