dualDistrib_apply — Mathlib

English

For f ∈ Dual M, g ∈ Dual N, and m ∈ M, n ∈ N, the action of dualDistrib on f ⊗ g evaluated at m ⊗ n is f(m) g(n).

Русский

Для f ∈ Dual M, g ∈ Dual N и m ∈ M, n ∈ N, применение dualDistrib к f ⊗ g на m ⊗ n даёт f(m) g(n).

LaTeX

$$$$ dualDistrib R M N (f \\otimes g) (m \\otimes n) = f(m) \\cdot g(n). $$$$

Lean4

@[simp]
theorem dualDistrib_apply (f : Dual R M) (g : Dual R N) (m : M) (n : N) :
    dualDistrib R M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * g n :=
  rfl

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