oreDiv_add_oreDiv — Mathlib

English

For any r, r' in X and s, s' in S with h: s'b*s = r*b*s', we have r / s + r' / s' = (s'' • r + r'' • r') /ₒ (s'' * s) where s'' = oreNum(s) s' and r'' = oreDenom(s) s'.

Русский

Для любых r, r' ∈ X и s, s' ∈ S с существующими witness-ами, имеющими sb*s = rb*s', выполняется формула сложения: r / s + r' / s' = (sb • r + rb • r') /ₒ (sb * s).

LaTeX

$$$\forall r,r' \in X\,\forall s,s' \in S\,\forall rb \in R\,\forall sb \in S,\ h: sb*s = rb*s'\; \Rightarrow\; r /ₒ s + r' /ₒ s' = (sb \cdot r + rb \cdot r') /ₒ (sb * s)$$$

Lean4

theorem oreDiv_add_oreDiv {r r' : X} {s s' : S} :
    r /ₒ s + r' /ₒ s' = (oreDenom (s : R) s' • r + oreNum (s : R) s' • r') /ₒ (oreDenom (s : R) s' * s) := by
  with_unfolding_all rfl

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