Commit 2025-06-04 03:03 bf709e0b

View on Github →

feat(AlternatingMap): define AlternatingMap.uncurryFin. (#25001)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.predAbove_predAbove_succAbove

added theorem Fin.succAbove_succAbove_predAbove

added theorem Fin.succAbove_succAbove_succAbove_predAbove

Modified Mathlib/Data/Fin/Parity.lean

added theorem Fin.neg_one_pow_succAbove_add_predAbove

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

added theorem Fin.removeNth_apply

added theorem Fin.removeNth_removeNth_eq_swap

added theorem Fin.removeNth_removeNth_heq_swap

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

added def AlternatingMap.toMultilinearMapLM

Modified Mathlib/LinearAlgebra/Alternating/Curry.lean

modified def AlternatingMap.curryLeft

modified def AlternatingMap.curryLeftLinearMap

modified theorem AlternatingMap.curryLeft_add

added theorem AlternatingMap.curryLeft_apply_apply

modified theorem AlternatingMap.curryLeft_compAlternatingMap

modified theorem AlternatingMap.curryLeft_compLinearMap

modified theorem AlternatingMap.curryLeft_same

modified theorem AlternatingMap.curryLeft_smul

modified theorem AlternatingMap.curryLeft_zero

Created Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean

added theorem AlternatingMap.map_insertNth

added theorem AlternatingMap.neg_one_pow_smul_map_insertNth

added theorem AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

added def AlternatingMap.uncurryFin

added def AlternatingMap.uncurryFinLM

added theorem AlternatingMap.uncurryFin_add

added theorem AlternatingMap.uncurryFin_apply

added theorem AlternatingMap.uncurryFin_curryLeft

added theorem AlternatingMap.uncurryFin_smul

added theorem AlternatingMap.uncurryFin_uncurryFinLM_comp_of_symmetric

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean