Theorem isSelfAdjoint_conjugate_iff_of_isUnit'

Modification history

2025-10-18 19:47

Mathlib/Algebra/Star/SelfAdjoint.lean

feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) …

Deleted isSelfAdjoint_conjugate_iff_of_isUnit'View on Github →

2025-09-01 17:39

Mathlib/Algebra/Star/SelfAdjoint.lean

feat(Algebra/Star/SelfAdjoint): `unit * a * star unit` is self-adjoint iff `a` is (#28544)

Added isSelfAdjoint_conjugate_iff_of_isUnit'View on Github →