Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_op

Modification history

2022-02-11 18:25
src/measure_theory/group/arithmetic.lean
feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593) …
Deleted measurable_opView on Github →
2021-11-19 12:03
src/measure_theory/group/arithmetic.lean
refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302) …
Modified measurable_opView on Github →
2021-10-29 13:53
src/measure_theory/group/arithmetic.lean
feat(measure_theory/group/arithmetic): add a section about `opposite` (#10026)
Added measurable_opView on Github →