Theorem ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric

Modification history

2025-10-04 09:36
Mathlib/Analysis/NormedSpace/Alternating/Uncurry/Fin.lean
feat(NormedSpace/Alternating/Uncurry/Fin): new file (#29957)
Added ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetricView on Github →