Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 19:52 289d17cd

View on Github →

chore(data/equiv/basic): avoid λ ⟨a, b⟩ in some defs, add simp lemmas (#3530)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.psigma_equiv_sigma_apply

added theorem equiv.psigma_equiv_sigma_symm_apply

modified def equiv.sigma_congr_left

added theorem equiv.sigma_congr_left_apply

added theorem equiv.sigma_congr_right_apply

added theorem equiv.sigma_congr_right_symm_apply

modified def equiv.sigma_equiv_prod

added theorem equiv.sigma_equiv_prod_apply

modified def equiv.sigma_equiv_prod_of_equiv

added theorem equiv.sigma_equiv_prod_symm_apply