oreDiv_add_char — Mathlib

English

For r,r' ∈ X and s,s' ∈ S with h: sb * s = rb * s', r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s).

Русский

Для любых r,r' ∈ X и s,s' ∈ S такие, что sb*s = rb*s', выполняется r / s + r' / s' = (sb • r + rb • r') / (sb * s).

LaTeX

$$$r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)$$$

Lean4

/-- A characterization of the addition on the Ore localization, allowing for arbitrary Ore
numerator and Ore denominator. -/
theorem oreDiv_add_char {r r' : X} (s s' : S) (rb : R) (sb : S) (h : sb * s = rb * s') :
    r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s) :=
  oreDiv_add_char' s s' rb sb h (sb * s).2

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