Zulip Chat Archive

Stream: Is there code for X?

Topic: Epi iff surjective in `Ab`.

Adam Topaz (Jan 11 2022 at 21:32):

We have docs#AddCommGroup.injective_of_mono but I can't seem to find the analogue for epi. Is this missing?

Adam Topaz (Jan 11 2022 at 22:41):

Well, I gave a fairly messy proof of this fact in the LTE repo here:
https://github.com/leanprover-community/lean-liquid/blob/95d8455fd9445a82d20b09ae4b3bd73052f53328/src/for_mathlib/ab_epi.lean#L52

Last updated: May 02 2025 at 03:31 UTC