Theorem Rat.cast_pos

Modification history

2024-06-09 12:00

Mathlib/Data/Rat/Cast/Order.lean

chore(Data/Rat/Cast/Order): Use `p`, `q` as variable names (#13644) …

Modified Rat.cast_pos View on Github →

2023-09-07 09:49

Mathlib/Data/Rat/Cast/Defs.lean

chore: split Data.Rat.Cast (#7001)

Modified Rat.cast_pos View on Github →

2023-01-04 12:39

Mathlib/Data/Rat/Cast.lean

feat: port data.rat.cast (#1261) …

Added Rat.cast_pos View on Github →