instMulActionAEEqFun — Mathlib

English

There is a MulAction structure on AEEqFun α β μ induced by DomMulAct M, with respect to the monoid structure on β and ContinuousAdd.

Русский

Существует структура MulAction на AEEqFun, индуцируемая DomMulAct M, совместимая с моноидной структурой β и непрерывным сложением.

LaTeX

$$MulAction (DomMulAct M) (AEEqFun α β μ)$$

Lean4

@[to_additive]
instance : MulAction Mᵈᵐᵃ (α →ₘ[μ] β)
    where
  one_smul := (AEEqFun.induction_on · fun _ _ ↦ by simp only [← mk_one, mk_smul_mk_aeeqFun, one_smul])
  mul_smul :=
    mk.surjective.forall.2 fun _ ↦
      mk.surjective.forall.2 fun _ ↦
        (AEEqFun.induction_on · fun _ _ ↦ by simp only [← mk_mul, mk_smul_mk_aeeqFun, mul_smul])

Похожие утверждения