English
The Ore condition is packaged as a witness triple (num, denom, eq).
Русский
Условие Оре упаковано в тройку (числитель, знаменатель, равенство).
LaTeX
$$oreCondition (r : R) (s : S) : Σ' r' : R, Σ' s' : S, s' * r = r' * s = ⟨oreNum r s, ⟨oreDenom r s, ore_eq r s⟩⟩$$
Lean4
/-- The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain
both witnesses and the condition for a given fraction. -/
@[to_additive AddOreLocalization.addOreCondition /--
The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain
both witnesses and the condition for a given difference. -/
]
def oreCondition (r : R) (s : S) : Σ' r' : R, Σ' s' : S, s' * r = r' * s :=
⟨oreNum r s, oreDenom r s, ore_eq r s⟩
