Theorems · Inductive type · functional analysis

ContinuousAlternatingMap

(R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_3) →
      Type u_4 →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [Module R M] →
              [TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] → [Module R N] → [TopologicalSpace N] → Type (max (max u_2 u_3) u_4)

A continuous alternating map from ι → M to N, denoted M [⋀^ι]→L[R] N, is a continuous map that is - multilinear : f (update m i (c • x)) = c • f (update m i x) and f (update m i (x + y)) = f (update m i x) + f (update m i y); - alternating : f v = 0 whenever v has two equal coordinates.

Defined in

Mathlib.Topology.Algebra.Module.Alternating.Basic

Cited by

292 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 5 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceAddCommMonoidModuleTopologicalSpace