Commit 2023-07-06 18:35 a691787c

View on Github →

feat: define continuous alternating maps (#5678)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Alternating.lean

added theorem AlternatingMap.mk_zero

Created Mathlib/Topology/Algebra/Module/Alternating.lean

added theorem ContinuousAlternatingMap.add_apply

added def ContinuousAlternatingMap.applyAddHom

added def ContinuousAlternatingMap.codRestrict

added theorem ContinuousAlternatingMap.coe_add

added theorem ContinuousAlternatingMap.coe_continuous

added theorem ContinuousAlternatingMap.coe_mk

added theorem ContinuousAlternatingMap.coe_neg

added theorem ContinuousAlternatingMap.coe_pi

added theorem ContinuousAlternatingMap.coe_restrictScalars

added theorem ContinuousAlternatingMap.coe_smul

added theorem ContinuousAlternatingMap.coe_sub

added theorem ContinuousAlternatingMap.coe_toAlternatingMap

added theorem ContinuousAlternatingMap.coe_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.coe_zero

added def ContinuousAlternatingMap.compContinuousLinearMap

added theorem ContinuousAlternatingMap.compContinuousLinearMap_apply

added def ContinuousAlternatingMap.compContinuousLinearMapₗ

added theorem ContinuousAlternatingMap.cons_add

added theorem ContinuousAlternatingMap.cons_smul

added def ContinuousAlternatingMap.constOfIsEmpty

added theorem ContinuousAlternatingMap.constOfIsEmpty_toAlternatingMap

added theorem ContinuousAlternatingMap.ext

added theorem ContinuousAlternatingMap.ext_iff

added theorem ContinuousAlternatingMap.map_add

added theorem ContinuousAlternatingMap.map_add_univ

added theorem ContinuousAlternatingMap.map_coord_zero

added theorem ContinuousAlternatingMap.map_eq_zero_of_eq

added theorem ContinuousAlternatingMap.map_eq_zero_of_not_injective

added theorem ContinuousAlternatingMap.map_piecewise_add

added theorem ContinuousAlternatingMap.map_piecewise_smul

added theorem ContinuousAlternatingMap.map_smul

added theorem ContinuousAlternatingMap.map_smul_univ

added theorem ContinuousAlternatingMap.map_sub

added theorem ContinuousAlternatingMap.map_sum

added theorem ContinuousAlternatingMap.map_sum_finset

added theorem ContinuousAlternatingMap.map_update_zero

added theorem ContinuousAlternatingMap.map_zero

added theorem ContinuousAlternatingMap.neg_apply

added def ContinuousAlternatingMap.ofSubsingleton

added theorem ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap

added def ContinuousAlternatingMap.pi

added def ContinuousAlternatingMap.piEquiv

added def ContinuousAlternatingMap.piLinearEquiv

added theorem ContinuousAlternatingMap.pi_apply

added def ContinuousAlternatingMap.prod

added theorem ContinuousAlternatingMap.range_toAlternatingMap

added theorem ContinuousAlternatingMap.range_toContinuousMultilinearMap

added def ContinuousAlternatingMap.restrictScalars

added def ContinuousAlternatingMap.smulRight

added theorem ContinuousAlternatingMap.smul_apply

added theorem ContinuousAlternatingMap.sub_apply

added theorem ContinuousAlternatingMap.sum_apply

added theorem ContinuousAlternatingMap.toAlternatingMap_add

added theorem ContinuousAlternatingMap.toAlternatingMap_injective

added theorem ContinuousAlternatingMap.toAlternatingMap_smul

added theorem ContinuousAlternatingMap.toAlternatingMap_zero

added def ContinuousAlternatingMap.toContinuousLinearMap

added def ContinuousAlternatingMap.toContinuousMultilinearMapLinear

added theorem ContinuousAlternatingMap.toContinuousMultilinearMap_add

added theorem ContinuousAlternatingMap.toContinuousMultilinearMap_injective

added theorem ContinuousAlternatingMap.toContinuousMultilinearMap_smul

added theorem ContinuousAlternatingMap.toContinuousMultilinearMap_zero

added def ContinuousAlternatingMap.toMultilinearAddHom

added theorem ContinuousAlternatingMap.vecCons_add

added theorem ContinuousAlternatingMap.vecCons_smul

added structure ContinuousAlternatingMap

added def ContinuousLinearEquiv.compContinuousAlternatingMap

added theorem ContinuousLinearEquiv.compContinuousAlternatingMap_coe

added def ContinuousLinearEquiv.continuousAlternatingMapComp

added def ContinuousLinearEquiv.continuousAlternatingMapCongr

added def ContinuousLinearMap.compContinuousAlternatingMap

added theorem ContinuousLinearMap.compContinuousAlternatingMap_coe

added def ContinuousLinearMap.compContinuousAlternatingMapₗ

added def ContinuousMultilinearMap.alternatization

added theorem ContinuousMultilinearMap.alternatization_apply_apply

added theorem ContinuousMultilinearMap.alternatization_apply_toAlternatingMap