coe_toIntLinearMap_ker

Mathlib.Algebra.Module.Submodule.Ker

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.coe_toIntLinearMap_ker

← MathLib Explorer

English

exists cosn over kernel equality in AddSubgroups, etc.

Русский

существуют равенства сумм и ядер в виде подгрупп аддитивных.

LaTeX

$$exists_ne_zero_of_sSup_eq_top$$

Lean4

@[simp]
theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
    LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker :=
  rfl

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

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

Разделы

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

Аффилиация

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