Theorem IsUnit.conjugate_nonneg_iff'

Modification history

2025-11-05 17:51
Mathlib/Algebra/Order/Star/Basic.lean
chore: rename **conjugate** to **star_left_conjugate** (#30692) …
Deleted IsUnit.conjugate_nonneg_iff'View on Github →
2025-10-18 19:47
Mathlib/Algebra/Order/Star/Basic.lean
feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) …
Added IsUnit.conjugate_nonneg_iff'View on Github →