Commit 2023-01-04 15:31 cfdf4320

View on Github →

chore: rename HasRatCast to RatCast (#1329)

Estimated changes

Modified Mathlib/Algebra/Field/Basic.lean

modified theorem ofDual_rat_cast

modified theorem ofLex_rat_cast

modified theorem toDual_rat_cast

modified theorem toLex_rat_cast

Modified Mathlib/Algebra/Field/Defs.lean

Modified Mathlib/Algebra/Order/Field/InjSurj.lean

Modified Mathlib/Algebra/Ring/ULift.lean

modified theorem ULift.rat_cast_down

Modified Mathlib/Data/Rat/Cast.lean

modified theorem Rat.cast_id