Def NNRat.castOrderEmbedding

Modification history

2024-06-09 07:15
Mathlib/Data/Rat/Cast/Order.lean
feat: order lemmas for NNRat (#13547) …
Added NNRat.castOrderEmbeddingView on Github →