ground_apply — Mathlib

English

For any f : M →ₚₗ[R] N and m ∈ M, ground(f)(m) equals the evaluation of f on 1 ⊗ m via the lid map.

Русский

Для любого f : M →ₚₗ[R] N и элемента m ∈ M грунт-f применим к m и равен значению f на 1 ⊗ m через отображение lid.

LaTeX

$$$f.ground(m) = \\operatorname{TensorProduct.lid} (R,N)\\bigl(f^{\\mathrm{toFun'}}(R, (1 \\otimes_{R} m))\\bigr).$$$

Lean4

theorem ground_apply (m : M) : f.ground m = TensorProduct.lid R N (f.toFun' R (1 ⊗ₜ[R] m)) :=
  rfl

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