Commit 2022-11-13 23:39 a48a5155

View on Github →

chore: fix names in algebra/group (#580) I might have missed a lemma or two, but I think that the folder is now good.

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem leftInverse_div_mul_left

added theorem leftInverse_inv

added theorem leftInverse_inv_mul_mul_right

added theorem leftInverse_mul_left_div

added theorem leftInverse_mul_right_inv_mul

deleted theorem left_inverse_div_mul_left

deleted theorem left_inverse_inv

deleted theorem left_inverse_inv_mul_mul_right

deleted theorem left_inverse_mul_left_div

deleted theorem left_inverse_mul_right_inv_mul

added theorem rightInverse_inv

deleted theorem right_inverse_inv

Modified Mathlib/Algebra/Group/Commute.lean