Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.sum_congr_trans

Modification history

2020-12-05 09:58

src/data/equiv/basic.lean

chore(data/equiv/basic): Add missing refl/trans/symm simp lemmas (#5223)

Added equiv.sum_congr_trans View on Github →