eqLocus_eq_ker_sub

Mathlib.Algebra.Module.Submodule.EqLocus

URI: https://scilib.ai/kg/mathlib#LinearMap.eqLocus_eq_ker_sub

English

For semilinear maps f, g, the equality locus equals the kernel of f − g.

Русский

Для полилинейных отображений f, g локус равенства равен ядру разности f − g.

LaTeX

$$$eqLocus(f,g) = \\ker (f - g)$$$

Lean4

theorem eqLocus_eq_ker_sub (f g : M →ₛₗ[τ₁₂] M₂) : eqLocus f g = ker (f - g) :=
  SetLike.ext fun _ => sub_eq_zero.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru