Zulip Chat Archive

Stream: PR reviews

Topic: Small and straightforward PRs


view this post on Zulip Johan Commelin (Dec 20 2018 at 08:16):

#531feat(data/int/basic) int.cast is ring hom [changes 1 file, +4 lines]
#532feat(ring_theory/subring) various lemmas [changes 1 file, +48 -2 lines]
#533feat(data/equiv/algebra) ring_equiv [changes 1 file, +31 -2 lines]
#534feat(ring_theory/ideal_operations) correspondence under surjection [changes 1 file, +47 lines]
#537feat(data/finsupp) frange [changes 1 file, +21 lines]
#540feat(order/filter): tendsto_at_top_at_top [changes 1 file, +10 lines]

view this post on Zulip Kenny Lau (Dec 20 2018 at 12:58):

@Mario Carneiro when are your christmas holidays?

view this post on Zulip Mario Carneiro (Dec 20 2018 at 12:59):

lol this is my chrismas holiday

view this post on Zulip Kenny Lau (Dec 20 2018 at 13:29):

all merged @Johan Commelin

view this post on Zulip Kenny Lau (Dec 20 2018 at 13:29):

thanks @Mario Carneiro

view this post on Zulip Johan Commelin (Dec 20 2018 at 14:02):

@Mario Carneiro Wow thanks!


Last updated: May 06 2021 at 13:21 UTC