one_div_mul'
plain-language theorem explainer
The identity (1/x) y = y/x holds for all real x and y. It is cited inside algebraic normalizations that must remain stable across mathlib releases. The proof is a one-line wrapper that invokes the ring tactic.
Claim. For all real numbers $x$ and $y$, $(1/x) y = y/x$.
background
The declaration resides in Compat.Mathlib, whose module documentation states that the file collects small alias lemmas and helpers to stabilize names across mathlib versions and reduce duplication. No upstream lemmas are referenced; the result is a direct re-statement of a basic field identity in ℝ.
proof idea
One-line wrapper that applies the ring tactic.
why it matters
It functions as a compatibility shim inside the Recognition Science codebase so that later algebraic steps do not depend on transient mathlib lemma names. No parent theorems or downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.