Theorem DomMulAct.mk_smul_mk_aeeqFun

Modification history

2023-07-06 09:30
Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean
feat: define action of `Mᵈᵐᵃ` on `α →ₘ[μ] β` (#5693) …
Added DomMulAct.mk_smul_mk_aeeqFunView on Github →