ker_restrictScalars — Mathlib

English

Let S be a semiring, M,N modules with R,S-scalar towers; for f : M →ₗ[S] N, the kernel after restricting scalars to R equals the restriction of the kernel: ker(f.restrictScalars R) = (ker f).restrictScalars R.

Русский

Пусть f : M →ₗ[S] N; тогда ядро после ограничения скаляров до R совпадает с ограниченным ядром: ker(f.restrictScalars R) = (ker f).restrictScalars R.

LaTeX

$$$\\ker(f\\restriction_R) = (\\ker f)\\restriction_R$$$

Lean4

@[simp]
theorem ker_restrictScalars (f : M →ₗ[S] N) :
    LinearMap.ker (f.restrictScalars R) = (LinearMap.ker f).restrictScalars R :=
  rfl

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