Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-01-15 02:19
7151fb70
View on Github →
chore(data/equiv/basic): equiv/perm_congr simp lemmas (
#5737
)
Estimated changes
Modified
src/data/equiv/basic.lean
added
theorem
equiv.equiv_congr_refl_left
added
theorem
equiv.equiv_congr_refl_right
added
theorem
equiv.perm_congr_def
added
theorem
equiv.perm_congr_symm
added
theorem
equiv.perm_congr_symm_apply