Theorem star_right_conjugate_le_conjugate

Modification history

2025-11-05 17:51

Mathlib/Algebra/Order/Star/Basic.lean

chore: rename **conjugate** to **star_left_conjugate** (#30692) …

Added star_right_conjugate_le_conjugate View on Github →