Commit 2023-03-29 05:49 10563d10

View on Github →

chore: re-port Mathlib.Algebra.Star.SelfAdjoint (#3159) This file was sufficiently far out of sync that it seemed sensible to just report it. A fresh output from mathport is included as a first commit; making it possible to diff both against the version in mathlib, and the version from mathlib. The change to Mathlib.Algebra.Star.Module was forgotten in #2926.

Estimated changes

added theorem IsSelfAdjoint.all
modified theorem IsSelfAdjoint.div
modified theorem IsSelfAdjoint.inv
modified theorem IsSelfAdjoint.isStarNormal
modified theorem IsSelfAdjoint.smul
modified theorem IsSelfAdjoint.zpow
added theorem isSelfAdjoint_intCast
added theorem isSelfAdjoint_natCast
added theorem isSelfAdjoint_ratCast
deleted theorem selfAdjoint.ratCast_mem
modified theorem selfAdjoint.val_zpow
modified def selfAdjoint
modified def skewAdjoint