instSMulCommClassAEEqFun_2 — Mathlib

English

Further establishment of commutativity of scalar actions on AEEqFun under multiple action assumptions.

Русский

Дальнейшее установление коммутативности действий на AEEqFun при нескольких условиях действия.

LaTeX

$$Instance: SMulCommClass (DomMulAct M) (DomMulAct N) (AEEqFun α β μ)$$

Lean4

@[to_additive]
instance [SMul N α] [MeasurableSMul N α] [SMulInvariantMeasure N α μ] [SMulCommClass M N α] :
    SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α →ₘ[μ] β) where
  smul_comm :=
    mk.surjective.forall.2 fun c₁ ↦
      mk.surjective.forall.2 fun c₂ ↦ (AEEqFun.induction_on · fun f hf ↦ by simp only [mk_smul_mk_aeeqFun, smul_comm])

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