quotKerEquivRange_apply_mk

Mathlib.LinearAlgebra.Isomorphisms

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

English

The canonical iso sends the class of x to f(x).

Русский

Каноническое изоморфизм отображает класс x в f(x).

LaTeX

$$(f.quotKerEquivRange (Submodule.Quotient.mk x) : M₂) = f x$$

Lean4

@[simp]
theorem quotKerEquivRange_apply_mk (x : M) : (f.quotKerEquivRange (Submodule.Quotient.mk x) : M₂) = f x :=
  rfl

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

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

Разделы

Аффилиация

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