Mathlib v3 is deprecated. Go to Mathlib v4

Def distrib_mul_action.to_add_equiv₀

Modification history

2023-07-28 12:48
src/group_theory/group_action/group.lean
feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863) …
Added distrib_mul_action.to_add_equiv₀View on Github →