_example

Mathlib.Analysis.CStarAlgebra.Module.Constructions

URI: https://scilib.ai/kg/mathlib#WithCStarModule._example

Lean4

example : instCStarModule (A := ℂ) = instCStarModuleComplex := by
  with_reducible_and_instances
    rfl
      /- Ensures that the two `Inner ℂ ℂ` instances are definitionally equal. Note that this cannot be at
      reducible and instances transparency because the one from `InnerProductSpace` uses `StarRingEnd`
      whereas `WithCStarModule.instCStarModule.toInner` uses `star` since `A` may not be commutative. -/

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

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

Разделы

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

Аффилиация

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