one_div_mul'
The equality (1/x) * y = y/x holds for all real x and y. It is invoked in any formal proof that must rewrite a product with a reciprocal as a quotient without expanding field axioms. The proof succeeds as a direct call to the ring tactic.
claimFor all real numbers $x$ and $y$, $(1/x) y = y/x$.
background
The module supplies compatibility shims and Mathlib imports to stabilize names across versions and cut duplication. This declaration concerns elementary real arithmetic with no extra structure imposed. No upstream lemmas appear in the dependency graph.
proof idea
One-line wrapper that applies the ring tactic.
why it matters in Recognition Science
The shim reduces duplication across the Recognition Science codebase by fixing a stable name for this identity. It supports algebraic steps needed in the broader development without linking to any specific forcing-chain theorem.
scope and limits
- Does not address division by zero.
- Does not extend to complex numbers or other fields.
- Does not supply a proof independent of Mathlib's ring solver.
formal statement (Lean)
30theorem one_div_mul' (x y : ℝ) : (1 / x) * y = y / x := by
proof body
One-line wrapper that applies ring.
31 ring
32