Mathlib v3 is deprecated. Go to Mathlib v4

Def rat.cast_order_embedding

Modification history

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