Commit 2025-03-12 17:40 7ec05b96

View on Github →

feat(Logic/Equiv/Fin): add finRotate lemma (#22251)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.one_le_of_ne_zero

added theorem Fin.val_sub_one_of_ne_zero

Modified Mathlib/Data/Fin/Tuple/Curry.lean

Modified Mathlib/Data/FinEnum/Option.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/TensorPower/Basic.lean

Renamed Mathlib/Logic/Equiv/Fin.lean to Mathlib/Logic/Equiv/Fin/Basic.lean

deleted theorem Fin.snoc_eq_cons_rotate

deleted theorem coe_finRotate

deleted theorem coe_finRotate_of_ne_last

deleted def finRotate

deleted theorem finRotate_apply_zero

deleted theorem finRotate_last'

deleted theorem finRotate_last

deleted theorem finRotate_of_lt

deleted theorem finRotate_one

deleted theorem finRotate_succ

deleted theorem finRotate_succ_apply

deleted theorem finRotate_zero

Created Mathlib/Logic/Equiv/Fin/Rotate.lean

added theorem Fin.snoc_eq_cons_rotate

added theorem coe_finRotate

added theorem coe_finRotate_of_ne_last

added theorem coe_finRotate_symm_of_ne_zero

added def finRotate

added theorem finRotate_apply_zero

added theorem finRotate_last'

added theorem finRotate_last

added theorem finRotate_of_lt

added theorem finRotate_one

added theorem finRotate_succ

added theorem finRotate_succ_apply

added theorem finRotate_succ_symm_apply

added theorem finRotate_symm_lt_iff_ne_zero

added theorem finRotate_zero

added theorem lt_finRotate_iff_ne_last

added theorem lt_finRotate_iff_ne_neg_one

Modified Mathlib/ModelTheory/Syntax.lean

Modified Mathlib/Order/Fin/Tuple.lean

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/Order/Partition/Equipartition.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean