PFR/Mathlib/MeasureTheory/Group/Arithmetic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Finset.measurable_prod'' line 16 source

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

    Statement uses: MeasurableSpace, CommMonoid, MeasurableMul₂, Finset, Membership.mem, Measurable, Prod, Function.HasUncurry.uncurry, Finset.prod

    Proof uses: Eq.mpr, id, Eq, congrArg, funext, Finset.prod_apply, Finset.measurable_prod, Measurable.fun_comp, Prod.fst, Prod.snd, Prod.mk, Measurable.prodMk, measurable_id'

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.