Commit 2025-10-08 02:50 1464c2e1

View on Github ā†’

feat: add lemmata about selfadjoint elements (#30301) This contains:

  • a NormedSpace š•œ (selfAdjoint E) instance.
  • ā€–x * xā€– = ā€–xā€– ^ 2 for selfadjoint x in a non-unital Cā‹†-ring.
  • some improved simp lemmas for realPart and imaginaryPart which supersede existing ones.

Estimated changes