mk₂_apply — Mathlib

English

Restriction by scalar towers preserves bilinearity under compatible scalar actions.

Русский

Ограничение по системам шкал сохраняет билинейность при совместимых скалярных действиях.

LaTeX

$$$ restrictScalars₁₂ (B) : M \\toₗ[R'] N \\toₗ[S'] P $ is bilinear$$

Lean4

@[simp]
theorem mk₂_apply (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) :
    (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] Nₗ →ₗ[R] Pₗ) m n = f m n :=
  rfl

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