instInvolutiveNeg

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

URI: https://scilib.ai/kg/mathlib#MeasureTheory.JordanDecomposition.instInvolutiveNeg

Lean4

instance instInvolutiveNeg : InvolutiveNeg (JordanDecomposition α)
    where
  neg j := ⟨j.negPart, j.posPart, j.mutuallySingular.symm⟩
  neg_neg _ := JordanDecomposition.ext rfl rfl

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

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

Разделы

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

Аффилиация

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