oreDiv_add_char' — Mathlib

English

Bundling all witnesses: the sum r / s + r' / s' is witnessed by some r'' ∈ R and s'' ∈ S with s'' * s = r'' * s' and the sum equality holds.

Русский

Обобщение witness-ов: сумма r / s + r' / s' имеет witnesses r'' ∈ R и s'' ∈ S такие, что s'' * s = r'' * s' и тождество суммы выполняется.

LaTeX

$$$\exists r'':R,\exists s'':S,\ s'' * s = r'' * s' \land r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s)$$$

Lean4

theorem oreDiv_add_char' {r r' : X} (s s' : S) (rb : R) (sb : R) (h : sb * s = rb * s') (h' : sb * s ∈ S) :
    r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * s, h'⟩ := by
  with_unfolding_all exact add''_char r s r' s' rb sb h h'

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