Commit 2023-03-17 15:06 5163d8ce

View on Github →

chore: Split off and golf ulift field instances (#2911) Match https://github.com/leanprover-community/mathlib/pull/18590 and https://github.com/leanprover-community/mathlib/pull/18596

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Field/ULift.lean

added theorem ULift.down_ratCast

added theorem ULift.up_ratCast

Modified Mathlib/Algebra/Group/ULift.lean

added theorem ULift.down_intCast

added theorem ULift.down_natCast

deleted theorem ULift.int_cast_down

deleted theorem ULift.nat_cast_down

added theorem ULift.up_intCast

added theorem ULift.up_natCast

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

deleted theorem Nonneg.nat_ceil_coe

deleted theorem Nonneg.nat_floor_coe

Created Mathlib/Algebra/Order/Nonneg/Floor.lean

added theorem Nonneg.nat_ceil_coe

added theorem Nonneg.nat_floor_coe

Modified Mathlib/Algebra/Ring/ULift.lean

deleted theorem ULift.rat_cast_down

Modified Mathlib/Data/Rat/NNRat.lean

Modified Mathlib/Data/Real/NNReal.lean