[Merged by Bors] - fix(Data/Rel): change what image_eq_cod_of_dom_subset states#35696
[Merged by Bors] - fix(Data/Rel): change what image_eq_cod_of_dom_subset states#35696GrigorenkoPV wants to merge 1 commit intoleanprover-community:masterfrom
image_eq_cod_of_dom_subset states#35696Conversation
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 02e8b79177Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
joneugster
left a comment
There was a problem hiding this comment.
Thank you for spotting this mistake!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by joneugster. |
|
Thanks! bors merge |
It used to be identical to its neighbor, `preimage_eq_dom_of_cod_subset`. Both lemmas seem to have been introduced in #25587. Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>
|
Pull request successfully merged into master. Build succeeded: |
image_eq_cod_of_dom_subset statesimage_eq_cod_of_dom_subset states
…rover-community#35696) It used to be identical to its neighbor, `preimage_eq_dom_of_cod_subset`. Both lemmas seem to have been introduced in leanprover-community#25587. Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>
It used to be identical to its neighbor,
preimage_eq_dom_of_cod_subset.Both lemmas seem to have been introduced in #25587.
I think this is technically a breaking change? Not sure what has to be done here.