Commit 2023-11-16 17:27 26fbe28d

View on Github →

chore(Algebra/Invertible/Defs): extract a variable command (#8441) As requested by @YaelDillies

Estimated changes

Modified Mathlib/Algebra/Invertible/Defs.lean

modified theorem invOf_mul_eq_iff_eq_mul_left

modified theorem mul_invOf_eq_iff_eq_mul_right

modified theorem mul_left_eq_iff_eq_invOf_mul

modified theorem mul_left_inj_of_invertible

modified theorem mul_right_eq_iff_eq_mul_invOf

modified theorem mul_right_inj_of_invertible