New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: make MulOpposite and AddOpposite structures #1036
Conversation
@@ -343,8 +351,10 @@ theorem op_div [Div α] (a b : α) : op (a / b) = op a / op b := | |||
rfl | |||
#align add_opposite.op_div AddOpposite.op_div | |||
|
|||
-- porting note: this lemma looked wrong to me -- is it wrong in mathlib3? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree, this is wrong in mathlib3. We didn't notice this because /
is the same operation on αᵃᵒᵖ
and α
and so it still works as a simp lemma.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not linting right now; I asked at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/possible.20linter.20bugs/near/316074640 |
bors merge |
This refactor makes `αᵐᵒᵖ` and `αᵃᵒᵖ` into structures with one field, an idea more appropriate in Lean 4 than the Lean 3 approach of type synonyms.
Pull request successfully merged into master. Build succeeded:
|
It turns out to be convenient to have `MulOpposite α = AddOpposite α` true by definition, in the same way that it is convenient to have `Additive α = α`; this means that we also get the defeq `AddOpposite (Additive α) = MulOpposite α`, which is convenient when working with quotients. This is a compromise between making `MulOpposite α = AddOpposite α = α` (what we had in Lean 3) and having no defeqs within those three types (which we had as of #1036). This is motivated by #3333
It turns out to be convenient to have `MulOpposite α = AddOpposite α` true by definition, in the same way that it is convenient to have `Additive α = α`; this means that we also get the defeq `AddOpposite (Additive α) = MulOpposite α`, which is convenient when working with quotients. This is a compromise between making `MulOpposite α = AddOpposite α = α` (what we had in Lean 3) and having no defeqs within those three types (which we had as of leanprover-community#1036). This is motivated by leanprover-community#3333
This refactor makes
αᵐᵒᵖ
andαᵃᵒᵖ
into structures with one field, an idea more appropriate in Lean 4 than the Lean 3 approach of type synonyms.