`one_div_mul'`

proved

show as: view math explainer →

module: IndisputableMonolith.Compat.Mathlib
domain: Compat
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Compat.Mathlib on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  27  exact Real.rpow_lt_one hx_pos.le hx_lt_one hy_pos
  28
  29-- Common simp-normalizations for division forms
  30theorem one_div_mul' (x y : ℝ) : (1 / x) * y = y / x := by
  31  ring
  32
  33theorem inv_pos_iff_one_div_pos' {x : ℝ} : (0 < x⁻¹) ↔ (0 < 1 / x) := by
  34  simp [one_div]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.