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_isUnitView 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_isUnitView on Github →