Commit 2025-11-24 18:21 288f2ca8
View on Github →fix(Algebra): fix mul order in le_inv_mul_iff₀' (#31982)
Before the fix, le_inv_mul_iff₀ and le_inv_mul_iff₀' had identical statement. The intention here should be swapping the mul in le_inv_mul_iff₀', similar to inv_mul_le_iff₀'