Commit 2023-12-15 17:44 fab6ab77
View on Github →fix: rename tsum_congr_subtype (#9080)
The lemma tsum_congr_subtype is currently stated in terms of set coercions rather than subtypes. This PR renames tsum_congr_subtype to tsum_congr_set_coe, and adds a new lemma tsum_congr_subtype whose statement is explicitly about subtypes.