Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-04-01 05:03
21cc8066
View on Github →
feat(data/equiv/basic):
perm_congr
group lemmas (
#6982
)
Estimated changes
Modified
src/data/equiv/basic.lean
modified
def
equiv.perm_congr
modified
theorem
equiv.perm_congr_apply
modified
theorem
equiv.perm_congr_def
added
theorem
equiv.perm_congr_refl
modified
theorem
equiv.perm_congr_symm
modified
theorem
equiv.perm_congr_symm_apply
added
theorem
equiv.perm_congr_trans
Modified
src/group_theory/perm/basic.lean
added
theorem
equiv.perm.perm_congr_eq_mul