extendScalarsOfIsLocalization_apply'

English

The extended map applied to x equals the original map applied to x, i.e., (f.extendScalarsOfIsLocalization S A) x = f x.

Русский

Расширенное отображение, применённое к x, равно исходному отображению, то есть (f.extendScalarsOfIsLocalization S A) x = f x.

LaTeX

$$$ (f.extendScalarsOfIsLocalization \\ S A) x = f x $$$

Lean4

@[simp]
theorem extendScalarsOfIsLocalization_apply' (f : M →ₗ[R] N) (x : M) : (f.extendScalarsOfIsLocalization S A) x = f x :=
  rfl

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