Mathlib v3 is deprecated. Go to Mathlib v4

Theorem rat.cast_pos_of_pos

Modification history

2022-08-23 10:32
src/data/rat/cast.lean
feat(data/rat/cast): add lemmas, golf (#16194) …
Added rat.cast_pos_of_posView on Github →