FLT/Mathlib/MeasureTheory/Group/Measure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measure

Material destined for Mathlib.

Imports (3)
Imported by 2 files
  1. lemma Topology.IsOpenEmbedding.isHaarMeasure_comap line 23 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Group, TopologicalSpace, MeasurableSpace, MeasurableMul, BorelSpace, MonoidHom, Topology.IsOpenEmbedding, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.Measure.comap

    Proof uses: MeasureTheory.Measure.IsHaarMeasure.mk, Topology.IsOpenEmbedding.isFiniteMeasureOnCompacts_comap, MeasurableEmbedding.isMulLeftInvariant_comap, Topology.IsOpenEmbedding.measurableEmbedding, MeasureTheory.Measure.IsOpenPosMeasure.comap

    17 instances, coercions and auxiliary constants left out.