Commit 2023-03-24 17:48 5c5703c2

View on Github →

feat: Missing opposite instances (#2940) Match https://github.com/leanprover-community/mathlib/pull/18602

Estimated changes

Modified Mathlib/Algebra/Field/Opposite.lean

added theorem MulOpposite.op_ratCast

added theorem MulOpposite.unop_ratCast

Modified Mathlib/Algebra/Group/Opposite.lean

added theorem MulOpposite.op_intCast

added theorem MulOpposite.op_natCast

added theorem MulOpposite.unop_intCast

added theorem MulOpposite.unop_natCast

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Opposite.lean

Modified Mathlib/Data/Int/Cast/Defs.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

deleted theorem MulOpposite.op_intCast

deleted theorem MulOpposite.unop_intCast

Modified Mathlib/Data/Nat/Cast/Basic.lean

deleted theorem MulOpposite.op_natCast

deleted theorem MulOpposite.unop_natCast

Modified Mathlib/Data/Rat/Cast.lean

deleted theorem MulOpposite.op_ratCast

deleted theorem MulOpposite.unop_ratCast