Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 09:37 46a70143

View on Github →

feat(data/equiv/basic): psigma_congr_right (#9687)

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.psigma_congr_right

added theorem equiv.psigma_congr_right_refl

added theorem equiv.psigma_congr_right_symm

added theorem equiv.psigma_congr_right_trans

modified def equiv.psigma_equiv_sigma

modified def equiv.sigma_congr_right

modified theorem equiv.sigma_congr_right_refl

modified theorem equiv.sigma_congr_right_symm

modified theorem equiv.sigma_congr_right_trans