Theorem conjugate_lt_conjugate'

Modification history

2025-11-05 17:51
Mathlib/Algebra/Order/Star/Basic.lean
chore: rename **conjugate** to **star_left_conjugate** (#30692) …
Deleted conjugate_lt_conjugate'View on Github →
2024-06-20 17:25
Mathlib/Algebra/Star/Order.lean
feat: `0 < c * a * star c` in `StarOrderedRing`s (#13975) …
Added conjugate_lt_conjugate'View on Github →