Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-08 06:49 c5ea4cdd

View on Github →

feat(group_theory/perm): define the permutation (0 1 ... (i : fin n)) (#6815) I tried a number of definitions and it looks like this is the least awkward one to prove with. In any case, using the API should allow you to avoid unfolding the definition.

Estimated changes

added theorem coe_fin_rotate
modified def fin_rotate
added theorem fin_rotate_apply_zero
modified theorem fin_rotate_last'
modified theorem fin_rotate_last
modified theorem fin_rotate_of_lt
added theorem fin_rotate_one
added theorem fin_rotate_succ_apply
added theorem fin_rotate_zero
added theorem fin.cast_le_zero
added theorem fin.coe_add_one
added theorem fin.coe_add_one_of_lt
added theorem fin.last_add_one
added theorem fin.range_cast_le
added theorem fin.range_cast_succ
added theorem fin.succ_eq_last_succ
added def fin.cycle_range
added theorem fin.cycle_range_apply
added theorem fin.cycle_range_last
added theorem fin.cycle_range_of_eq
added theorem fin.cycle_range_of_gt
added theorem fin.cycle_range_of_le
added theorem fin.cycle_range_of_lt
added theorem fin.cycle_range_self
added theorem fin.cycle_range_zero'
added theorem fin.cycle_range_zero
added theorem fin.sign_cycle_range
added theorem fin_rotate_succ
added theorem sign_fin_rotate