Commit 2022-12-28 14:53 bc2fc2dc

View on Github →

feat: port Algebra.Ring.Ulift (#1240) Most of the porting consists of doing by hand what pi_instance_derive_field did.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/ULift.lean

added theorem ULift.rat_cast_down

added def ULift.ringEquiv