Inverse_of_Division_Product
Proveddivisionproofwikirings
Let R be a commutative ring with unity. Let a, b be units. Then (a/b)⁻¹ = b/a.
Preamble
import Mathlib.Algebra.Field.Basic
Formal statement
theorem Inverse_of_Division_Product {F : Type _} [Field F] (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) : (a / b)⁻¹ = b / a := by sorrySource