add_oreDiv

Mathlib.RingTheory.OreLocalization.Basic

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

English

If r,r' ∈ X and s ∈ S, then r /ₒ s + r' /ₒ s = (r + r') /ₒ s.

Русский

Если r, r' ∈ X и s ∈ S, то r /ₒ s + r' /ₒ s = (r + r') /ₒ s.

LaTeX

$$$r /ₒ s + r' /ₒ s = (r + r') /ₒ s$$$

Lean4

@[simp]
theorem add_oreDiv {r r' : X} {s : S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s := by simp [oreDiv_add_char s s 1 1 (by simp)]

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

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

Разделы

Аффилиация

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