instCoeOut

Mathlib.LinearAlgebra.Eigenspace.Basic

URI: https://scilib.ai/kg/mathlib#Module.End.UnifEigenvalues.instCoeOut

English

There is a canonical coercion from UnifEigenvalues(f,k) to R given by the projection map.

Русский

Существует каноническое преобразование из UnifEigenvalues(f,k) в R, заданное проекцией.

LaTeX

$$instCoeOut {f} {k} : CoeOut (UnifEigenvalues f k) R$$

Lean4

instance instCoeOut {f : Module.End R M} (k : ℕ∞) : CoeOut (UnifEigenvalues f k) R where coe := UnifEigenvalues.val f k

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

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

Разделы

Аффилиация

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