requests for Rat

Stream: batteries

[Kim Morrison]

@Mario Carneiro, could we have

import Std.Data.Rat.Basic

namespace Rat

theorem normalize_eq_mk (n : Int) (d : Nat) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1) :
    normalize n d h = mk n d h c := by
  simp [normalize, c, maybeNormalize]

theorem normalize_eq_normalize_iff
    (a : Int) (b : Nat) (hb : b ≠ 0) (c : Int) (d : Nat) (hd : d ≠ 0) :
    normalize a b hb = normalize c d hd ↔ a * ↑d = c * ↑b := by
  sorry

in say Std.Data.Rat.Lemmas? These would be very helpful for the mathlib side of Rat.

[Mario Carneiro]

yes, most of the Rat lemmas are missing. Most of the theorems in data.rat.basic should end up in there eventually

[Kim Morrison]

Okay, I have proofs of these in Data.Rat.Basic. The proofs don't immediately lift to Std (using cases', etc), so I'll just leave these there for now.

[Mario Carneiro]

Cool, it will be a lot easier to migrate them once you have mostly working proofs already

[Mario Carneiro]

Cleaning up cases' etc is comparatively easy