Theorems · Definition · number theory

AbstractMeasure

(X : Type u_1) →
  (R : Type u_3) →
    (E : Type u_4) →
      [TopologicalSpace X] →
        [inst : AddCommGroup E] →
          [TopologicalSpace E] →
            [inst_2 : CommRing R] →
              [inst_3 : TopologicalSpace R] → [IsTopologicalRing R] → [Module R E] → Type (max (max u_3 u_1) u_4)

The space of E-valued measures on X, i.e. continuous linear maps C(X, R) → E. (The case R = E is the most important case.) This is the same space C(X, R) →L[R] E, but we do not want it to inherit the default (norm) topology, so we make a type synonym.

Defined in

Mathlib.NumberTheory.Padics.Measure.Basic

Cited by

20 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRingModule