Zulip Chat Archive

Stream: PR reviews

Topic: Small and straightforward PRs

Johan Commelin (Dec 20 2018 at 08:16):

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

Kenny Lau (Dec 20 2018 at 12:58):

@Mario Carneiro when are your christmas holidays?

Mario Carneiro (Dec 20 2018 at 12:59):

lol this is my chrismas holiday

Kenny Lau (Dec 20 2018 at 13:29):

all merged @Johan Commelin

Kenny Lau (Dec 20 2018 at 13:29):

thanks @Mario Carneiro

Johan Commelin (Dec 20 2018 at 14:02):

@Mario Carneiro Wow thanks!

Last updated: Dec 20 2023 at 11:08 UTC