Zulip Chat Archive

Stream: mathlib4

Topic: Injective

Scott Morrison (Oct 24 2022 at 22:59):

I will make the PR that updates master to use Injective and Surjective, and the @Yakov Pechersky can merge and update his PRs.

Yakov Pechersky (Oct 24 2022 at 23:00):

Would you like to do it in mathlib#498?

Yakov Pechersky (Oct 24 2022 at 23:03):

What are lemmas like LeftInverse.injective to be named now? as is?

Scott Morrison (Oct 24 2022 at 23:06):

as is

Scott Morrison (Oct 24 2022 at 23:15):

mathlib4#501

Yakov Pechersky (Oct 24 2022 at 23:15):

I'm going to hold off on my port PRs until that's merged

Scott Morrison (Oct 24 2022 at 23:17):

Sorry about the confusion. I think I will merge the capitalisation PR as soon as CI accepts it, so you can unblock all of yours.

Scott Morrison (Oct 24 2022 at 23:54):

@Yakov Pechersky, #501 has hit master if you want to update your PRs.

Yakov Pechersky (Oct 24 2022 at 23:59):

mathlib4#496 is updated

Yakov Pechersky (Oct 25 2022 at 00:08):

mathlib4#487 is updated

Yakov Pechersky (Oct 25 2022 at 00:09):

mathlib4#493 is updated

Yakov Pechersky (Oct 25 2022 at 00:23):

mathlib4#497 is updated

Yakov Pechersky (Oct 25 2022 at 00:42):

mathlib4#482 is updated

Scott Morrison (Oct 25 2022 at 00:45):

Yakov Pechersky said:

mathlib4#482 is updated

Could you update the PR description? Some things there are no longer true (e.g. no convert, for one).

Yakov Pechersky (Oct 25 2022 at 00:46):

Sure thing!

Last updated: Dec 20 2023 at 11:08 UTC