piScalarRight_apply — Mathlib

English

There is a simp lemma stating piScalarRight_apply: piScalarRight R S N ι x = piScalarRightHom R S N ι x.

Русский

Существует упрощённая лемма: piScalarRight_apply: piScalarRight R S N ι x = piScalarRightHom R S N ι x.

LaTeX

$$$piScalarRight_apply : \piScalarRight(R,S,N,\iota) \; x = \piScalarRightHom(R,S,N,\iota)\; x.$$$

Lean4

@[simp]
theorem piScalarRight_apply (x : N ⊗[R] (ι → R)) : piScalarRight R S N ι x = piScalarRightHom R S N ι x := by rfl

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