comp_codRestrict

Mathlib.Algebra.Module.Submodule.LinearMap

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

← MathLib Explorer

English

The inclusion map p.subtype is the same map as the function Subtype.val.

Русский

Включение p.subtype совпадает с функцией Subtype.val.

LaTeX

$$$p.subtype = Subtype.val$$$

Lean4

@[simp]
theorem comp_codRestrict (p : Submodule R₃ M₃) (h : ∀ b, g b ∈ p) :
    ((codRestrict p g h).comp f : M →ₛₗ[σ₁₃] p) = codRestrict p (g.comp f) fun _ => h _ :=
  ext fun _ => rfl

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

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

Разделы

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

Аффилиация

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