Commit 2021-01-04 16:47 7d0b9882

View on Github →

chore(data/equiv/basic): Add refl / symm / trans lemmas for equiv_congr (#5609) We already have this triplet of lemmas for sum_congr and sigma_congr.

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.equiv_congr_refl

added theorem equiv.equiv_congr_symm

added theorem equiv.equiv_congr_trans