Zulip Chat Archive
Stream: general
Topic: sum_fin_add_comm_equiv
Paul van Wamelen (Mar 21 2021 at 21:13):
Shouldn't
def sum_fin_sum_equiv : fin m ⊕ fin n ≃ fin (m + n)
be called sum_fin_add_equiv?
Alex J. Best (Mar 21 2021 at 22:01):
Or fin_sum_fin_equiv?
Last updated: May 02 2025 at 03:31 UTC