Commit 2025-08-14 14:33 b9adabfb

View on Github →

chore(Algebra/GroupWithZero/Units): golf entire eq_mul_of_inv_mul_eq₀ and eq_mul_of_mul_inv_eq₀ (#28391)

Estimated changes

modified theorem eq_mul_of_inv_mul_eq₀
modified theorem eq_mul_of_mul_inv_eq₀