Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 12:17 900ce6fc

View on Github →

chore(data/equiv/basic): rename involutive.to_equiv to to_perm (#12486)

Estimated changes

Modified src/algebra/quandle.lean

Modified src/algebra/star/basic.lean

Modified src/data/equiv/basic.lean

modified def equiv.perm

added theorem function.involutive.coe_to_perm

deleted def function.involutive.to_equiv

added def function.involutive.to_perm

added theorem function.involutive.to_perm_involutive

added theorem function.involutive.to_perm_symm

Modified src/data/equiv/module.lean

Modified src/data/equiv/mul_add.lean