ofIsCompl_zero

Mathlib.LinearAlgebra.Projection

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

English

If h is IsCompl(p,q), then the linear map with φ=0 and ψ=0 is the zero map on E.

Русский

Пусть h = IsCompl(p,q); карта with φ=0 и ψ=0 есть нулевая карта на E.

LaTeX

$$$ofIsCompl\ h\ 0\ 0 = 0.$$$

Lean4

@[simp]
theorem ofIsCompl_zero (h : IsCompl p q) : (ofIsCompl h 0 0 : E →ₗ[R] F) = 0 :=
  ofIsCompl_eq _ (fun _ => rfl) fun _ => rfl

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

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

Разделы

Аффилиация

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