Commit 2023-04-28 02:33 b9cc405b

View on Github →

feat: port Topology.Algebra.Module.Multilinear (#3348)

Estimated changes

Modified Mathlib.lean

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

added def ContinuousLinearMap.compContinuousMultilinearMap

added theorem ContinuousLinearMap.compContinuousMultilinearMap_coe

added def ContinuousMultilinearMap.Simps.apply

added theorem ContinuousMultilinearMap.add_apply

added def ContinuousMultilinearMap.applyAddHom

added theorem ContinuousMultilinearMap.coe_coe

added theorem ContinuousMultilinearMap.coe_continuous

added theorem ContinuousMultilinearMap.coe_pi

added theorem ContinuousMultilinearMap.coe_restrictScalars

added def ContinuousMultilinearMap.compContinuousLinearMap

added theorem ContinuousMultilinearMap.compContinuousLinearMap_apply

added theorem ContinuousMultilinearMap.cons_add

added theorem ContinuousMultilinearMap.cons_smul

added def ContinuousMultilinearMap.constOfIsEmpty

added theorem ContinuousMultilinearMap.ext

added theorem ContinuousMultilinearMap.ext_iff

added theorem ContinuousMultilinearMap.map_add

added theorem ContinuousMultilinearMap.map_add_univ

added theorem ContinuousMultilinearMap.map_coord_zero

added theorem ContinuousMultilinearMap.map_piecewise_add

added theorem ContinuousMultilinearMap.map_piecewise_smul

added theorem ContinuousMultilinearMap.map_smul

added theorem ContinuousMultilinearMap.map_smul_univ

added theorem ContinuousMultilinearMap.map_sub

added theorem ContinuousMultilinearMap.map_sum

added theorem ContinuousMultilinearMap.map_sum_finset

added theorem ContinuousMultilinearMap.map_zero

added theorem ContinuousMultilinearMap.mkPiAlgebraFin_apply

added theorem ContinuousMultilinearMap.mkPiAlgebra_apply

added theorem ContinuousMultilinearMap.neg_apply

added def ContinuousMultilinearMap.ofSubsingleton

added def ContinuousMultilinearMap.pi

added def ContinuousMultilinearMap.piEquiv

added def ContinuousMultilinearMap.piLinearEquiv

added theorem ContinuousMultilinearMap.pi_apply

added def ContinuousMultilinearMap.prod

added theorem ContinuousMultilinearMap.prod_apply

added def ContinuousMultilinearMap.restrictScalars

added def ContinuousMultilinearMap.smulRight

added theorem ContinuousMultilinearMap.smul_apply

added theorem ContinuousMultilinearMap.sub_apply

added theorem ContinuousMultilinearMap.sum_apply

added def ContinuousMultilinearMap.toContinuousLinearMap

added def ContinuousMultilinearMap.toMultilinearMapLinear

added theorem ContinuousMultilinearMap.toMultilinearMap_add

added theorem ContinuousMultilinearMap.toMultilinearMap_injective

added theorem ContinuousMultilinearMap.toMultilinearMap_smul

added theorem ContinuousMultilinearMap.toMultilinearMap_zero

added theorem ContinuousMultilinearMap.zero_apply

added structure ContinuousMultilinearMap