pi_apply — Mathlib

English

Under suitable SMulCommClass assumptions, CMMap is a central scalar object with respect to ring actions.

Русский

При подходящих условиях SMulCommClass, CMMap имеет центральный скаляр по отношению к скалярному действию колец.

LaTeX

$$$\\text{IsCentralScalar } R' (\\mathrm{ContinuousMultilinearMap} A M_1 M_2)$$$

Lean4

theorem pi_apply {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
    [∀ i, Module R (M' i)] (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) (m : ∀ i, M₁ i) (j : ι') :
    pi f m j = f j m :=
  rfl

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