English
Bundling witnesses: a sigma-type encoding of witnesses (r'', s'') such that s'' * s = r'' * s' and the addition formula holds.
Русский
Упаковка свидетелей: сигма-тип кодирует свидетели (r'', s'') такие, что s'' * s = r'' * s' и формула сложения выполняется.
LaTeX
$$$\text{oreDivAddChar'}(r,r',s,s') = \Sigma' r'' : R, \Sigma' s'' : S, s'' * s = r'' * s' ∧ r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s)$$$
Lean4
/-- Another characterization of the addition on the Ore localization, bundling up all witnesses
and conditions into a sigma type. -/
def oreDivAddChar' (r r' : X) (s s' : S) :
Σ' r'' : R, Σ' s'' : S, s'' * s = r'' * s' ∧ r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s) :=
⟨oreNum (s : R) s', oreDenom (s : R) s', ore_eq (s : R) s', oreDiv_add_oreDiv⟩
