instNNRatCast

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#selfAdjoint.instNNRatCast

English

There is a canonical NN rational cast for self-adjoint elements, preserving self-adjointness.

Русский

Существует каноническое отображение NNRat в самосопряжённые элементы, сохраняющее самосопряжённость.

LaTeX

$$$\text{NNRatCast} : \mathrm{NNRatCast}(\mathrm{selfAdjoint}(R))$$$

Lean4

instance instNNRatCast : NNRatCast (selfAdjoint R) where nnratCast q := ⟨q, .nnratCast q⟩

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

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

Разделы

Аффилиация

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