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(data/quot,data/set/basic): add lemmas about lift
#17699
Conversation
* Add `Quot.surjective_lift` and `Quotient.surjective_liftOn'`. * This is the `mathlib4` version of leanprover-community/mathlib#17699.
begin | ||
rw [matrix.to_linear_map₂, linear_map.to_matrix₂, linear_equiv.symm_trans_apply, | ||
←matrix.to_linear_map₂'], | ||
simp [matrix.to_linear_map₂'_apply], | ||
end |
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.
Can you either mention this in the PR description or remove it from the PR?
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.
Was this intended as a fixup to #17705?
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.
Yes, I've got a timeout and fixed it.
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.
bors d+
Thanks!
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
* Add `quot.surjective_lift`, `quotient.surjective_lift_on'`. * Mark `quot.lift_mk` as `simp`. * Add `set.range_quot_lift`, `set.range_quotient_lift`, `set.range_quotient_mk'`, and `set.range_quotient_lift_on'`. * The `mathlib4` version: leanprover-community/mathlib4#701. * Prove `matrix.to_linear_map₂_apply` by `rfl`.
This PR was included in a batch that was canceled, it will be automatically retried |
* Add `quot.surjective_lift`, `quotient.surjective_lift_on'`. * Mark `quot.lift_mk` as `simp`. * Add `set.range_quot_lift`, `set.range_quotient_lift`, `set.range_quotient_mk'`, and `set.range_quotient_lift_on'`. * The `mathlib4` version: leanprover-community/mathlib4#701. * Prove `matrix.to_linear_map₂_apply` by `rfl`.
Pull request successfully merged into master. Build succeeded: |
lift
lift
quot.surjective_lift
,quotient.surjective_lift_on'
.quot.lift_mk
assimp
.set.range_quot_lift
,set.range_quotient_lift
,set.range_quotient_mk'
, andset.range_quotient_lift_on'
.mathlib4
version: [Merged by Bors] - feat(Data/Quot): add 2 lemmas mathlib4#701.matrix.to_linear_map₂_apply
byrfl
.