-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - chore(*): speed up slow proofs #7253
Conversation
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.
LGTM to me. Thanks so much for resolving these slow proofs!
add_comm := by {intros, ext, unfold coe_fn has_coe_to_fun.coe sesq, rw add_comm} } | ||
sesq_smul_right := λ a x y, by rw [sesq_smul_right, mul_neg_eq_neg_mul_symm] }⟩ | ||
|
||
instance : add_comm_group (sesq_form R M I) := |
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.
Shouldn't this get a dedicated nsmul
field now?
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.
They get one for free, which is the naive one defined by induction. One should only add one by hand if there is a risk of diamond, i.e., if we ever consider sesquilinear forms over naturals or integers. Sesquilinear forms over naturals don't make sense, so there is no issue here. There is an issue over the integers, so we should probably add a gsmul
field, yes. I'll do it in #7255.
Thanks 🎉 bors merge |
Proofs that are too slow for the forthcoming `gsmul` refactor. I learnt that `by convert ...` is extremely useful even to close a goal, when elaboration using the expected type is a bad idea.
Pull request successfully merged into master. Build succeeded: |
Proofs that are too slow for the forthcoming
gsmul
refactor. I learnt thatby convert ...
is extremely useful even to close a goal, when elaboration using the expected type is a bad idea.