map

Mathlib.LinearAlgebra.SModEq

URI: https://scilib.ai/kg/mathlib#SModEq.map

← MathLib Explorer

English

If x ≡ y mod U and f is linear, then f(x) ≡ f(y) mod U.map f.

Русский

Если x ≡ y mod U и f линейно, тогда f(x) ≡ f(y) mod U.map f.

LaTeX

$$$$ x \\equiv y\\ [SMOD\\ U] \\Rightarrow f x \\equiv f y\\ [SMOD\\ (U.map\\ f)]. $$$$

Lean4

theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] :=
  (Submodule.Quotient.eq _).2 <| f.map_sub x y ▸ mem_map_of_mem <| (Submodule.Quotient.eq _).1 hxy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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