Theorem ofLex_rat_cast

Modification history

2024-04-05 21:50
Mathlib/Algebra/Field/Basic.lean
chore(Field/InjSurj): Tidy (#11480) …
Deleted ofLex_rat_castView on Github →
2023-01-04 15:31
Mathlib/Algebra/Field/Basic.lean
chore: rename HasRatCast to RatCast (#1329)
Modified ofLex_rat_castView on Github →
2022-12-17 23:54
Mathlib/Algebra/Field/Basic.lean
chore: tidy various files (#1086)
Added ofLex_rat_castView on Github →