Theorem DomMulAct.smul_aeeqFun_aeeq

Modification history

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