Basic

📁 Source: Mathlib/Topology/Algebra/Module/Alternating/Basic.lean

Statistics

Metric	Count
Definitions addCommMonoid, applyAddHom, codRestrict, compContinuousLinearMap, compContinuousLinearMapₗ, constOfIsEmpty, funLike, instAdd, instAddCommGroup, instDistribMulAction, instInhabited, instModule, instMulAction, instNeg, instSMul, instSub, instZero, ofSubsingleton, pi, piEquiv, piLinearEquiv, prod, restrictScalars, smulRight, toAlternatingMap, toAlternatingMapLinear, toContinuousLinearMap, toContinuousMultilinearMap, toContinuousMultilinearMapLinear, toMultilinearAddHom, uniqueOfCommRing, continuousAlternatingMapCongrEquiv, continuousAlternatingMapCongrLeftEquiv, continuousAlternatingMapCongrRightEquiv, compContinuousAlternatingMap, compContinuousAlternatingMapₗ, alternatization, «term_[⋀^_]→L[_]_»	38
Theorems add_apply, codRestrict_apply_coe, coe_add, coe_continuous, coe_mk, coe_neg, coe_pi, coe_restrictScalars, coe_smul, coe_sub, coe_toAlternatingMap, coe_toContinuousMultilinearMap, coe_zero, compContinuousLinearMap_apply, compContinuousLinearMapₗ_apply, cons_add, cons_smul, constOfIsEmpty_apply, constOfIsEmpty_toAlternatingMap, constOfIsEmpty_toContinuousMultilinearMap, continuousMapClass, ext, ext_iff, ext_ring, ext_ring_iff, instIsCentralScalar, instIsScalarTower, instSMulCommClass, map_add_univ, map_coord_zero, map_eq_zero_of_eq, map_eq_zero_of_eq', map_eq_zero_of_not_injective, map_piecewise_add, map_piecewise_smul, map_smul_univ, map_sum, map_sum_finset, map_update_add, map_update_smul, map_update_sub, map_update_zero, map_vecCons_sub, map_zero, neg_apply, ofSubsingleton_apply_apply, ofSubsingleton_apply_toContinuousMultilinearMap, ofSubsingleton_symm_apply_apply, ofSubsingleton_toAlternatingMap, piEquiv_apply, piEquiv_symm_apply, piLinearEquiv_apply, piLinearEquiv_symm_apply, pi_apply, prod_apply, range_toAlternatingMap, range_toContinuousMultilinearMap, smulRight_apply, smulRight_toContinuousMultilinearMap, smul_apply, sub_apply, sum_apply, toAlternatingMapLinear_apply, toAlternatingMap_add, toAlternatingMap_injective, toAlternatingMap_smul, toAlternatingMap_zero, toContinuousLinearMap_apply, toContinuousMultilinearMapLinear_apply, toContinuousMultilinearMap_add, toContinuousMultilinearMap_injective, toContinuousMultilinearMap_smul, toContinuousMultilinearMap_zero, toMultilinearAddHom_apply, vecCons_add, vecCons_smul, compContinuousAlternatingMap_coe, continuousAlternatingMapCongrLeftEquiv_apply, continuousAlternatingMapCongrRightEquiv_apply, compContinuousAlternatingMap_coe, alternatization_apply_apply, alternatization_apply_toAlternatingMap, alternatization_apply_toContinuousMultilinearMap	83
Total	121

ContinuousAlternatingMap

Definitions

Name	Category	Theorems
addCommMonoid 📖	CompOp	68 math math: hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, ContinuousMultilinearMap.alternatization_apply_apply, hasStrictFDerivAt_compContinuousLinearMap, compContinuousLinearMapₗ_apply, piLIE_apply_apply, toAlternatingMapLinear_apply, curryLeft_smul, HasFDerivWithinAt.continuousAlternatingMap_apply, toAlternatingMap_curryLeft, fderiv_continuousAlternatingMapCompContinuousLinearMap, fderiv_continuousAlternatingMap_apply, HasFDerivAt.continuousAlternatingMap_apply, curryLeft_apply_apply, alternatizeUncurryFin_smul, alternatizeUncurryFin_constOfIsEmptyLIE_comp, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, norm_curryLeft, apply_apply, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, norm_alternatizeUncurryFinCLM_le, AlternatingMap.mkContinuousAlternating_norm_le, curryLeft_compContinuousAlternatingMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, curryLeft_compContinuousLinearMap, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm, toContinuousMultilinearMapLinear_apply, toContinuousMultilinearMapCLM_apply, fderivCompContinuousLinearMapCLM_apply, toAlternatingMap_alternatizeUncurryFin, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, sum_apply, HasStrictFDerivAt.continuousAlternatingMap_apply, curryLeft_same, curryLeft_zero, toContinuousMultilinearMap_curryLeft, piLIE_symm_apply_apply, piLinearEquiv_symm_apply, restrictScalarsCLM_apply, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply, ContinuousMultilinearMap.alternatization_apply_toAlternatingMap, fderivCompContinuousLinearMap_apply, curryLeft_add, prodLIE_apply, AlternatingMap.mkContinuousLinear_norm_le, curryLeftLI_apply, fderivCompContinuousLinearMap_of_isEmpty, norm_alternatizeUncurryFin_le, AlternatingMap.mkContinuousAlternating_norm_le_max, ContinuousLinearEquiv.continuousAlternatingMapCongr_apply, alternatizeUncurryFin_add, fderivWithin_continuousAlternatingMap_apply, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, liftCLM_apply, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, prodLIE_symm_apply, AlternatingMap.mkContinuousLinear_norm_le_max, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, piLinearEquiv_apply, compContinuousLinearMapCLM_apply, AlternatingMap.mkContinuousAlternating_apply, alternatizeUncurryFin_apply, toMultilinearAddHom_apply, alternatizeUncurryFinCLM_apply, ContinuousLinearMap.flipAlternating_apply_apply
applyAddHom 📖	CompOp	—
codRestrict 📖	CompOp	1 math math: codRestrict_apply_coe
compContinuousLinearMap 📖	CompOp	18 math math: hasStrictFDerivAt_compContinuousLinearMap, DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap, extDerivWithin_pullback, compContinuousLinearMapₗ_apply, fderiv_continuousAlternatingMapCompContinuousLinearMap, ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv_apply, DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, curryLeft_compContinuousLinearMap, compContinuousLinearMap_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply, extDeriv_pullback, ContinuousLinearEquiv.continuousAlternatingMapCongr_apply, norm_compContinuousLinearMap_le, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, compContinuousLinearMapCLM_apply
compContinuousLinearMapₗ 📖	CompOp	1 math math: compContinuousLinearMapₗ_apply
constOfIsEmpty 📖	CompOp	8 math math: extDeriv_constOfIsEmpty, norm_constOfIsEmpty, constOfIsEmpty_toAlternatingMap, constOfIsEmptyLIE_apply, extDerivWithin_constOfIsEmpty, constOfIsEmpty_toContinuousMultilinearMap, constOfIsEmpty_apply, nnnorm_constOfIsEmpty
funLike 📖	CompOp	119 math math: cons_add, uniformContinuous_eval_const, ContinuousMultilinearMap.alternatization_apply_apply, vecCons_smul, tsum_eval, map_insertNth, le_mul_prod_of_opNorm_le_of_le, fderiv_continuousAlternatingMap_apply_const, smul_apply, piLIE_apply_apply, coe_pi, map_coord_zero, HasFDerivWithinAt.continuousAlternatingMap_apply, le_opNNNorm, hasSum_eval, DifferentiableAt.continuousAlternatingMap_apply_const, fderiv_continuousAlternatingMap_apply, ContinuousLinearEquiv.compContinuousAlternatingMap_coe, HasFDerivAt.continuousAlternatingMap_apply, AlternatingMap.coe_mkContinuous, curryLeft_apply_apply, coe_smul, fderivWithin_continuousAlternatingMap_apply_const_apply, DifferentiableWithinAt.continuousAlternatingMap_apply_const, extDeriv_apply_vectorField, coe_sub, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, map_piecewise_smul, map_update_sub, le_opNorm, map_update_add, apply_apply, add_apply, map_sum, map_sum_finset, extDerivWithin_apply_vectorField_of_pairwise_commute, map_zero, sub_apply, constOfIsEmptyLIE_symm_apply, hasStrictFDerivAt, map_update_smul, DifferentiableAt.continuousAlternatingMap_apply, le_opNorm_mul_pow_of_le, prod_apply, pi_apply, ContinuousLinearMap.compContinuousAlternatingMap_coe, HasFDerivAt.continuousAlternatingMap_apply_const, hasBasis_nhds_zero, DifferentiableOn.continuousAlternatingMap_apply, uniformContinuous_coe_fun, extDerivWithin_apply_vectorField, sum_apply, map_add_univ, ext_iff, HasStrictFDerivAt.continuousAlternatingMap_apply, cons_smul, vecCons_add, norm_image_sub_le', piLIE_symm_apply_apply, le_opNorm_mul_pow_card_of_le, fderiv_continuousAlternatingMap_apply_apply, le_of_opNorm_le, compContinuousLinearMap_apply, coe_mk, ofSubsingleton_apply_apply, fderivWithin_continuousAlternatingMap_apply_apply, coe_zero, Differentiable.continuousAlternatingMap_apply_const, map_vecCons_sub, hasBasis_nhds_zero_of_basis, fderivWithin_continuousAlternatingMap_apply_const, constOfIsEmpty_apply, ext_ring_iff, map_eq_zero_of_not_injective, fderivCompContinuousLinearMap_apply, neg_apply, opNorm_le_iff, map_piecewise_add, extDeriv_apply_vectorField_of_pairwise_commute, coe_toContinuousMultilinearMap, DifferentiableWithinAt.continuousAlternatingMap_apply, hasFDerivWithinAt, map_eq_zero_of_eq, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, map_update_zero, HasStrictFDerivAt.continuousAlternatingMap_apply_const, toContinuousLinearMap_apply, DifferentiableOn.continuousAlternatingMap_apply_const, fderivWithin_continuousAlternatingMap_apply, differentiable, continuousMapClass, coe_neg, neg_one_pow_smul_map_insertNth, unit_le_opNorm, extDerivWithin_apply, opNNNorm_le_iff, liftCLM_apply, bound, Differentiable.continuousAlternatingMap_apply, coe_restrictScalars, map_smul_univ, instContinuousEval, coe_toAlternatingMap, hasFDerivAt, coe_continuous, fderiv_continuousAlternatingMap_apply_const_apply, coe_add, AlternatingMap.mkContinuousAlternating_apply, alternatizeUncurryFin_apply, ratio_le_opNorm, ofSubsingleton_symm_apply_apply, HasFDerivWithinAt.continuousAlternatingMap_apply_const, instContinuousEvalConst, norm_image_sub_le, smulRight_apply, extDeriv_apply, le_of_opNNNorm_le, ContinuousLinearMap.flipAlternating_apply_apply, le_opNorm_mul_prod_of_le
instAdd 📖	CompOp	10 math math: extDerivWithin_fun_add, extDerivWithin_add, add_apply, extDeriv_add, extDeriv_fun_add, curryLeft_add, toAlternatingMap_add, alternatizeUncurryFin_add, toContinuousMultilinearMap_add, coe_add
instAddCommGroup 📖	CompOp	10 math math: hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, instIsUniformAddGroup, hasStrictFDerivAt_compContinuousLinearMap, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, instIsTopologicalAddGroup, norm_alternatizeUncurryFinCLM_le, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, fderivCompContinuousLinearMapCLM_apply, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, alternatizeUncurryFinCLM_apply
instDistribMulAction 📖	CompOp	2 math math: curryLeft_smul, alternatizeUncurryFin_smul
instInhabited 📖	CompOp	—
instModule 📖	CompOp	59 math math: hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasStrictFDerivAt_compContinuousLinearMap, compContinuousLinearMapₗ_apply, piLIE_apply_apply, toAlternatingMapLinear_apply, curryLeft_smul, toAlternatingMap_curryLeft, constOfIsEmptyLIE_apply, ofSubsingletonLIE_symm_apply, curryLeft_apply_apply, alternatizeUncurryFin_smul, alternatizeUncurryFin_constOfIsEmptyLIE_comp, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, norm_curryLeft, apply_apply, norm_alternatizeUncurryFinCLM_le, AlternatingMap.mkContinuousAlternating_norm_le, curryLeft_compContinuousAlternatingMap, ofSubsingletonLIE_apply, toContinuousMultilinearMapLI_apply, constOfIsEmptyLIE_symm_apply, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, curryLeft_compContinuousLinearMap, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm, toContinuousMultilinearMapLinear_apply, toContinuousMultilinearMapCLM_apply, fderivCompContinuousLinearMapCLM_apply, toAlternatingMap_alternatizeUncurryFin, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, curryLeft_same, curryLeft_zero, restrictScalarsLI_apply, toContinuousMultilinearMap_curryLeft, piLIE_symm_apply_apply, piLinearEquiv_symm_apply, restrictScalarsCLM_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply, fderivCompContinuousLinearMap_apply, curryLeft_add, prodLIE_apply, AlternatingMap.mkContinuousLinear_norm_le, curryLeftLI_apply, fderivCompContinuousLinearMap_of_isEmpty, norm_alternatizeUncurryFin_le, AlternatingMap.mkContinuousAlternating_norm_le_max, ContinuousLinearEquiv.continuousAlternatingMapCongr_apply, alternatizeUncurryFin_add, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, liftCLM_apply, prodLIE_symm_apply, AlternatingMap.mkContinuousLinear_norm_le_max, alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, piLinearEquiv_apply, compContinuousLinearMapCLM_apply, AlternatingMap.mkContinuousAlternating_apply, alternatizeUncurryFin_apply, alternatizeUncurryFinCLM_apply, ContinuousLinearMap.flipAlternating_apply_apply
instMulAction 📖	CompOp	—
instNeg 📖	CompOp	2 math math: neg_apply, coe_neg
instSMul 📖	CompOp	16 math math: smul_apply, curryLeft_smul, extDeriv_fun_smul, instContinuousSMul, instContinuousConstSMul, coe_smul, alternatizeUncurryFin_smul, instUniformContinuousConstSMul, toAlternatingMap_smul, extDerivWithin_fun_smul, extDeriv_smul, extDerivWithin_smul, instIsCentralScalar, instSMulCommClass, toContinuousMultilinearMap_smul, instIsScalarTower
instSub 📖	CompOp	2 math math: coe_sub, sub_apply
instZero 📖	CompOp	13 math math: extDeriv_extDeriv, extDerivWithin_extDerivWithin_eqOn, toContinuousMultilinearMap_zero, hasBasis_nhds_zero, toAlternatingMap_zero, curryLeft_same, curryLeft_zero, coe_zero, hasBasis_nhds_zero_of_basis, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, extDerivWithin_extDerivWithin_apply, extDeriv_extDeriv_apply, alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero
ofSubsingleton 📖	CompOp	15 math math: extDeriv_constOfIsEmpty, norm_ofSubsingleton_id_le, extDerivWithin_constOfIsEmpty, ofSubsingletonLIE_symm_apply, ofSubsingleton_apply_toContinuousMultilinearMap, alternatizeUncurryFin_constOfIsEmptyLIE_comp, ofSubsingletonLIE_apply, norm_ofSubsingleton, nnnorm_ofSubsingleton_id, ofSubsingleton_apply_apply, norm_ofSubsingleton_id, nnnorm_ofSubsingleton, nnnorm_ofSubsingleton_id_le, ofSubsingleton_toAlternatingMap, ofSubsingleton_symm_apply_apply
pi 📖	CompOp	6 math math: opNNNorm_pi, coe_pi, piEquiv_apply, pi_apply, opNorm_pi, piLinearEquiv_apply
piEquiv 📖	CompOp	2 math math: piEquiv_apply, piEquiv_symm_apply
piLinearEquiv 📖	CompOp	2 math math: piLinearEquiv_symm_apply, piLinearEquiv_apply
prod 📖	CompOp	4 math math: opNorm_prod, prod_apply, prodLIE_apply, opNNNorm_prod
restrictScalars 📖	CompOp	8 math math: isEmbedding_restrictScalars, norm_restrictScalars, isUniformEmbedding_restrictScalars, continuous_restrictScalars, restrictScalarsLI_apply, restrictScalarsCLM_apply, coe_restrictScalars, uniformContinuous_restrictScalars
smulRight 📖	CompOp	2 math math: smulRight_toContinuousMultilinearMap, smulRight_apply
toAlternatingMap 📖	CompOp	12 math math: toAlternatingMapLinear_apply, constOfIsEmpty_toAlternatingMap, toAlternatingMap_injective, toAlternatingMap_curryLeft, toAlternatingMap_smul, toAlternatingMap_alternatizeUncurryFin, toAlternatingMap_zero, range_toAlternatingMap, ContinuousMultilinearMap.alternatization_apply_toAlternatingMap, toAlternatingMap_add, coe_toAlternatingMap, ofSubsingleton_toAlternatingMap
toAlternatingMapLinear 📖	CompOp	2 math math: toAlternatingMapLinear_apply, toAlternatingMap_alternatizeUncurryFin
toContinuousLinearMap 📖	CompOp	6 math math: HasFDerivWithinAt.continuousAlternatingMap_apply, fderiv_continuousAlternatingMap_apply, HasFDerivAt.continuousAlternatingMap_apply, HasStrictFDerivAt.continuousAlternatingMap_apply, toContinuousLinearMap_apply, fderivWithin_continuousAlternatingMap_apply
toContinuousMultilinearMap 📖	CompOp	30 math math: isClosedEmbedding_toContinuousMultilinearMap, hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, isUniformEmbedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap, ofSubsingleton_apply_toContinuousMultilinearMap, isEmbedding_toContinuousMultilinearMap, toContinuousMultilinearMapLI_apply, toContinuousMultilinearMap_zero, hasStrictFDerivAt, map_eq_zero_of_eq', range_toContinuousMultilinearMap, norm_toContinuousMultilinearMap, toContinuousMultilinearMapLinear_apply, toContinuousMultilinearMapCLM_apply, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, smulRight_toContinuousMultilinearMap, toContinuousMultilinearMap_curryLeft, uniformContinuous_toContinuousMultilinearMap, toContinuousMultilinearMap_injective, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, constOfIsEmpty_toContinuousMultilinearMap, nnnorm_toContinuousMultilinearMap, coe_toContinuousMultilinearMap, hasFDerivWithinAt, toContinuousMultilinearMap_smul, toContinuousMultilinearMap_add, hasFDerivAt, continuous_toContinuousMultilinearMap, enorm_toContinuousMultilinearMap, toMultilinearAddHom_apply
toContinuousMultilinearMapLinear 📖	CompOp	1 math math: toContinuousMultilinearMapLinear_apply
toMultilinearAddHom 📖	CompOp	1 math math: toMultilinearAddHom_apply
uniqueOfCommRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
codRestrict_apply_coe 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousAlternatingMap funLike	Submodule.addCommMonoid Submodule.module instTopologicalSpaceSubtype codRestrict	—	—
coe_add 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_continuous 📖	mathematical	—	Continuous Pi.topologicalSpace DFunLike.coe ContinuousAlternatingMap funLike	—	ContinuousMultilinearMap.cont
coe_mk 📖	mathematical	MultilinearMap.toFun ContinuousMultilinearMap.toMultilinearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe ContinuousAlternatingMap funLike ContinuousMultilinearMap ContinuousMultilinearMap.funLike	—	—
coe_neg 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_pi 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace funLike pi	—	—
coe_restrictScalars 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike restrictScalars	—	—
coe_smul 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coe_sub 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_toAlternatingMap 📖	mathematical	—	DFunLike.coe AlternatingMap AlternatingMap.instFunLike toAlternatingMap ContinuousAlternatingMap funLike	—	—
coe_toContinuousMultilinearMap 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike toContinuousMultilinearMap ContinuousAlternatingMap funLike	—	—
coe_zero 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
compContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike compContinuousLinearMap ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—
compContinuousLinearMapₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike compContinuousLinearMapₗ compContinuousLinearMap	—	smulCommClass_self
cons_add 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Fin.cons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.cons_add
cons_smul 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Fin.cons SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.cons_smul
constOfIsEmpty_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike constOfIsEmpty	—	—
constOfIsEmpty_toAlternatingMap 📖	mathematical	—	toAlternatingMap constOfIsEmpty AlternatingMap.constOfIsEmpty	—	—
constOfIsEmpty_toContinuousMultilinearMap 📖	mathematical	—	toContinuousMultilinearMap constOfIsEmpty ContinuousMultilinearMap.constOfIsEmpty	—	—
continuousMapClass 📖	mathematical	—	ContinuousMapClass ContinuousAlternatingMap Pi.topologicalSpace funLike	—	ContinuousMultilinearMap.cont
ext 📖	—	DFunLike.coe ContinuousAlternatingMap funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike	—	ext
ext_ring 📖	—	DFunLike.coe ContinuousAlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	toAlternatingMap_injective AlternatingMap.ext_ring
ext_ring_iff 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_ring
instIsCentralScalar 📖	mathematical	—	IsCentralScalar ContinuousAlternatingMap instSMul MulOpposite MulOpposite.instMonoid ContinuousConstSMul.op SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul SMulCommClass.op_right MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ContinuousConstSMul.op SMulCommClass.op_right ext IsCentralScalar.op_smul_eq_smul
instIsScalarTower 📖	mathematical	—	IsScalarTower ContinuousAlternatingMap instSMul	—	ext smul_assoc
instSMulCommClass 📖	mathematical	—	SMulCommClass ContinuousAlternatingMap instSMul	—	ext SMulCommClass.smul_comm
map_add_univ 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.sum Finset Finset.univ Finset.fintype Finset.piecewise Finset.decidableMem	—	MultilinearMap.map_add_univ
map_coord_zero 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe ContinuousAlternatingMap funLike	—	MultilinearMap.map_coord_zero
map_eq_zero_of_eq 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_eq_zero_of_eq'
map_eq_zero_of_eq' 📖	mathematical	—	MultilinearMap.toFun ContinuousMultilinearMap.toMultilinearMap toContinuousMultilinearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
map_eq_zero_of_not_injective 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	AlternatingMap.map_eq_zero_of_not_injective
map_piecewise_add 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Finset.piecewise Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.decidableMem Finset.sum Finset Finset.powerset	—	MultilinearMap.map_piecewise_add
map_piecewise_smul 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap CommSemiring.toSemiring funLike Finset.piecewise SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.decidableMem Finset.prod CommSemiring.toCommMonoid	—	MultilinearMap.map_piecewise_smul
map_smul_univ 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap CommSemiring.toSemiring funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommSemiring.toCommMonoid Finset.univ	—	MultilinearMap.map_smul_univ
map_sum 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Finset.sum Finset.univ Pi.instFintype	—	MultilinearMap.map_sum
map_sum_finset 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Finset.sum Fintype.piFinset	—	MultilinearMap.map_sum_finset
map_update_add 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Function.update AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.map_update_add'
map_update_smul 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Function.update SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.map_update_smul'
map_update_sub 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike Function.update SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	MultilinearMap.map_update_sub
map_update_zero 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Function.update AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	MultilinearMap.map_update_zero
map_vecCons_sub 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike Matrix.vecCons SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Matrix.vecCons.eq_1 Fin.update_cons_zero map_update_sub
map_zero 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	MultilinearMap.map_zero
neg_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
ofSubsingleton_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.funLike	—	—
ofSubsingleton_apply_toContinuousMultilinearMap 📖	mathematical	—	toContinuousMultilinearMap DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousMultilinearMap ContinuousMultilinearMap.ofSubsingleton	—	—
ofSubsingleton_symm_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike Equiv ContinuousAlternatingMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofSubsingleton funLike	—	—
ofSubsingleton_toAlternatingMap 📖	mathematical	—	toAlternatingMap DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton LinearMap AlternatingMap AlternatingMap.ofSubsingleton ContinuousLinearMap.toLinearMap	—	—
piEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace EquivLike.toFunLike Equiv.instEquivLike piEquiv pi	—	—
piEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace EquivLike.toFunLike Equiv.instEquivLike Equiv.symm piEquiv ContinuousLinearMap.compContinuousAlternatingMap ContinuousLinearMap.proj	—	—
piLinearEquiv_apply 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousConstSMul	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace addCommMonoid Pi.continuousAdd AddSemigroup.toAdd instModule instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Pi.smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike piLinearEquiv pi	—	RingHomInvPair.ids Pi.continuousAdd instContinuousConstSMulForall Pi.smulCommClass
piLinearEquiv_symm_apply 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousConstSMul	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace addCommMonoid Pi.continuousAdd AddSemigroup.toAdd instModule instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Pi.smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piLinearEquiv ContinuousLinearMap.compContinuousAlternatingMap ContinuousLinearMap.proj	—	RingHomInvPair.ids Pi.continuousAdd instContinuousConstSMulForall Pi.smulCommClass
pi_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Pi.addCommMonoid Pi.module Pi.topologicalSpace funLike pi	—	—
prod_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd funLike prod	—	—
range_toAlternatingMap 📖	mathematical	—	Set.range AlternatingMap ContinuousAlternatingMap toAlternatingMap setOf Continuous Pi.topologicalSpace DFunLike.coe AlternatingMap.instFunLike	—	Set.ext ContinuousMultilinearMap.cont AlternatingMap.map_eq_zero_of_eq' DFunLike.ext'
range_toContinuousMultilinearMap 📖	mathematical	—	Set.range ContinuousMultilinearMap ContinuousAlternatingMap toContinuousMultilinearMap setOf	—	Set.ext map_eq_zero_of_eq'
smulRight_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap CommSemiring.toSemiring funLike smulRight SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
smulRight_toContinuousMultilinearMap 📖	mathematical	—	toContinuousMultilinearMap CommSemiring.toSemiring smulRight ContinuousMultilinearMap.smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
smul_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
sub_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
sum_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Finset.sum addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
toAlternatingMapLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap AlternatingMap addCommMonoid AlternatingMap.instAddCommMonoid instModule AlternatingMap.instModule LinearMap.instFunLike toAlternatingMapLinear toAlternatingMap	—	—
toAlternatingMap_add 📖	mathematical	—	toAlternatingMap ContinuousAlternatingMap instAdd AlternatingMap AlternatingMap.instAdd	—	—
toAlternatingMap_injective 📖	mathematical	—	ContinuousAlternatingMap AlternatingMap toAlternatingMap	—	DFunLike.ext' DFunLike.ext'_iff
toAlternatingMap_smul 📖	mathematical	—	toAlternatingMap ContinuousAlternatingMap instSMul AlternatingMap AlternatingMap.instSMul	—	—
toAlternatingMap_zero 📖	mathematical	—	toAlternatingMap ContinuousAlternatingMap instZero AlternatingMap AlternatingMap.instZero	—	—
toContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike toContinuousLinearMap ContinuousAlternatingMap funLike Function.update	—	—
toContinuousMultilinearMapLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap ContinuousMultilinearMap addCommMonoid ContinuousMultilinearMap.addCommMonoid instModule ContinuousMultilinearMap.instModule LinearMap.instFunLike toContinuousMultilinearMapLinear toContinuousMultilinearMap	—	—
toContinuousMultilinearMap_add 📖	mathematical	—	toContinuousMultilinearMap ContinuousAlternatingMap instAdd ContinuousMultilinearMap ContinuousMultilinearMap.instAdd	—	—
toContinuousMultilinearMap_injective 📖	mathematical	—	ContinuousAlternatingMap ContinuousMultilinearMap toContinuousMultilinearMap	—	—
toContinuousMultilinearMap_smul 📖	mathematical	—	toContinuousMultilinearMap ContinuousAlternatingMap instSMul ContinuousMultilinearMap ContinuousMultilinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
toContinuousMultilinearMap_zero 📖	mathematical	—	toContinuousMultilinearMap ContinuousAlternatingMap instZero ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	—
toMultilinearAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom ContinuousAlternatingMap ContinuousMultilinearMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid ContinuousMultilinearMap.addCommMonoid AddMonoidHom.instFunLike toMultilinearAddHom toContinuousMultilinearMap	—	—
vecCons_add 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Matrix.vecCons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.cons_add
vecCons_smul 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap funLike Matrix.vecCons SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.cons_smul

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
continuousAlternatingMapCongrEquiv 📖	CompOp	—
continuousAlternatingMapCongrLeftEquiv 📖	CompOp	1 math math: continuousAlternatingMapCongrLeftEquiv_apply
continuousAlternatingMapCongrRightEquiv 📖	CompOp	2 math math: compContinuousAlternatingMap_coe, continuousAlternatingMapCongrRightEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousAlternatingMap_coe 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap ContinuousAlternatingMap.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike continuousAlternatingMapCongrRightEquiv ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids equivLike	—	RingHomInvPair.ids
continuousAlternatingMapCongrLeftEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousAlternatingMap EquivLike.toFunLike Equiv.instEquivLike continuousAlternatingMapCongrLeftEquiv ContinuousAlternatingMap.compContinuousLinearMap toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids symm	—	RingHomInvPair.ids
continuousAlternatingMapCongrRightEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousAlternatingMap EquivLike.toFunLike Equiv.instEquivLike continuousAlternatingMapCongrRightEquiv ContinuousLinearMap.compContinuousAlternatingMap toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousAlternatingMap 📖	CompOp	12 math math: LinearIsometry.norm_compContinuousAlternatingMap, ContinuousAlternatingMap.isUniformInducing_postcomp, ContinuousAlternatingMap.piEquiv_symm_apply, ContinuousAlternatingMap.curryLeft_compContinuousAlternatingMap, compContinuousAlternatingMap_coe, ContinuousAlternatingMap.piLinearEquiv_symm_apply, norm_compContinuousAlternatingMap_le, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv_apply, ContinuousLinearEquiv.continuousAlternatingMapCongr_apply, compContinuousAlternatingMapCLM_apply_apply, ContinuousAlternatingMap.prodLIE_symm_apply
compContinuousAlternatingMapₗ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousAlternatingMap_coe 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap ContinuousAlternatingMap.funLike compContinuousAlternatingMap ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	—

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
alternatization 📖	CompOp	3 math math: alternatization_apply_apply, alternatization_apply_toContinuousMultilinearMap, alternatization_apply_toAlternatingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatization_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap AddCommGroup.toAddCommMonoid ContinuousAlternatingMap.funLike AddMonoidHom ContinuousMultilinearMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.addCommMonoid AddMonoidHom.instFunLike alternatization Finset.sum Equiv.Perm Finset.univ Equiv.instFintype Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign funLike EquivLike.toFunLike Equiv.instEquivLike	—	IsTopologicalAddGroup.toContinuousAdd sum_apply Finset.sum_congr
alternatization_apply_toAlternatingMap 📖	mathematical	—	ContinuousAlternatingMap.toAlternatingMap AddCommGroup.toAddCommMonoid DFunLike.coe AddMonoidHom ContinuousMultilinearMap ContinuousAlternatingMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.addCommMonoid AddMonoidHom.instFunLike alternatization MultilinearMap AlternatingMap SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MultilinearMap.instAddCommGroup AlternatingMap.instAddCommGroup MultilinearMap.alternatization toMultilinearMap	—	AlternatingMap.ext IsTopologicalAddGroup.toContinuousAdd alternatization_apply_apply Finset.sum_congr MultilinearMap.alternatization_apply
alternatization_apply_toContinuousMultilinearMap 📖	mathematical	—	ContinuousAlternatingMap.toContinuousMultilinearMap AddCommGroup.toAddCommMonoid DFunLike.coe AddMonoidHom ContinuousMultilinearMap ContinuousAlternatingMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.addCommMonoid AddMonoidHom.instFunLike alternatization Finset.sum Equiv.Perm Finset.univ Equiv.instFintype Units Int.instMonoid Units.instSMul instSMul DistribMulAction.toDistribSMul Module.toDistribMulAction Int.instSemiring AddCommGroup.toIntModule MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign domDomCongr	—	IsTopologicalAddGroup.toContinuousAdd

(root)

Definitions

Name	Category	Theorems
«term_[⋀^_]→L[_]_» 📖	CompOp	—

---

← Back to Index