mk_apply — Mathlib

English

The application of mk is linear in each argument; mk(m + m')(n) = mk(m)(n) + mk(m')(n) and mk(m)(n+n') = mk(m)(n) + mk(m)(n').

Русский

Применение mk линейно по каждому аргументу: mk(m + m')(n) = mk(m)(n) + mk(m')(n) и mk(m)(n+n') = mk(m)(n) + mk(m)(n').

LaTeX

$$$\forall m,m',n:\; \text{mk}(m+m')(n) = \text{mk}(m)(n) + \text{mk}(m')(n)$ and $\text{mk}(m)(n+n') = \text{mk}(m)(n) + \text{mk}(m)(n')$$$

Lean4

@[simp]
theorem mk_apply (m : M) (n : N) : mk R M N m n = m ⊗ₜ n :=
  rfl

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