Theorem star_left_conjugate_pos

Modification history

2025-11-05 17:51
Mathlib/Algebra/Order/Star/Basic.lean
chore: rename **conjugate** to **star_left_conjugate** (#30692) …
Added star_left_conjugate_posView on Github →