ore_eq — Mathlib

English

The Ore condition of a fraction: oreDenom(r,s) · r = oreNum(r,s) · s.

Русский

Условие Оре дроби: oreDenom(r,s) · r = oreNum(r,s) · s.

LaTeX

$$oreDenom(r,s) * r = oreNum(r,s) * s$$

Lean4

/-- The Ore condition of a fraction, expressed in terms of `oreNum` and `oreDenom`. -/
@[to_additive AddOreLocalization.add_ore_eq /--
    The Ore condition of a difference, expressed in terms of `oreMin` and `oreSubtra`. -/
    ]
theorem ore_eq (r : R) (s : S) : oreDenom r s * r = oreNum r s * s :=
  OreSet.ore_eq r s

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