Commit 2025-10-04 09:36 b4264fbd

View on Github →

feat(NormedSpace/Alternating/Uncurry/Fin): new file (#29957)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Alternating/Uncurry/Fin.lean

added theorem ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_add

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_apply

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_smul

added theorem ContinuousAlternatingMap.map_insertNth

added theorem ContinuousAlternatingMap.neg_one_pow_smul_map_insertNth

added theorem ContinuousAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

added theorem ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le

added theorem ContinuousAlternatingMap.norm_alternatizeUncurryFin_le

added theorem ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin

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

added def AlternatingMap.alternatizeUncurryFin

added def AlternatingMap.alternatizeUncurryFinLM

added theorem AlternatingMap.alternatizeUncurryFin_add

added theorem AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric

added theorem AlternatingMap.alternatizeUncurryFin_apply

added theorem AlternatingMap.alternatizeUncurryFin_curryLeft

added theorem AlternatingMap.alternatizeUncurryFin_smul

deleted def AlternatingMap.uncurryFin

deleted def AlternatingMap.uncurryFinLM

deleted theorem AlternatingMap.uncurryFin_add

deleted theorem AlternatingMap.uncurryFin_apply

deleted theorem AlternatingMap.uncurryFin_curryLeft

deleted theorem AlternatingMap.uncurryFin_smul

deleted theorem AlternatingMap.uncurryFin_uncurryFinLM_comp_of_symmetric