Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 09:58 c5009dd7

View on Github →

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

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.sigma_congr_right_refl

added theorem equiv.sigma_congr_right_symm

added theorem equiv.sigma_congr_right_trans

added theorem equiv.sum_congr_refl

added theorem equiv.sum_congr_trans