Commit 2023-09-06 11:21 d67f31e1

View on Github →

chore: split Mathlib.Algebra.Invertible (#6973) Mathlib.Algebra.Invertible is used by fundamental tactics, and this essentially splits it into the part used by NormNum, and everything else.

Estimated changes

deleted theorem inv_mul_cancel
deleted theorem inv_ne_zero
deleted theorem mul_inv_cancel_left₀
deleted theorem mul_inv_cancel_right₀
added theorem mul_inv_cancel_left₀
added theorem inv_mul_cancel
added theorem inv_ne_zero
deleted theorem Commute.invOf_left
deleted theorem Commute.invOf_right
deleted theorem Invertible.congr
deleted def Invertible.copy'
deleted def Invertible.copy
deleted def Invertible.map
deleted def Invertible.mul
deleted def Invertible.mulLeft
deleted def Invertible.mulRight
deleted theorem Ring.inverse_invertible
deleted def Units.invertible
deleted theorem commute_invOf
deleted theorem div_self_of_invertible
deleted theorem invOf_div
deleted theorem invOf_eq_group_inv
deleted theorem invOf_eq_inv
deleted theorem invOf_eq_left_inv
deleted theorem invOf_eq_right_inv
deleted theorem invOf_inj
deleted theorem invOf_invOf
deleted theorem invOf_mul
deleted theorem invOf_mul_self'
deleted theorem invOf_mul_self
deleted theorem invOf_mul_self_assoc'
deleted theorem invOf_mul_self_assoc
deleted theorem invOf_neg
deleted theorem invOf_one'
deleted theorem invOf_one
deleted theorem invOf_two_add_invOf_two
deleted theorem invOf_units
deleted def invertibleDiv
deleted def invertibleInv
deleted def invertibleMul
deleted def invertibleNeg
deleted def invertibleOfGroup
deleted def invertibleOfNonzero
deleted def invertibleOne
deleted theorem invertible_unique
deleted theorem isUnit_of_invertible
deleted theorem map_invOf
deleted theorem mul_invOf_mul_self_cancel
deleted theorem mul_invOf_self'
deleted theorem mul_invOf_self
deleted theorem mul_invOf_self_assoc'
deleted theorem mul_invOf_self_assoc
deleted theorem mul_mul_invOf_self_cancel
deleted theorem nonzero_of_invertible
deleted theorem one_sub_invOf_two
deleted theorem pos_of_invertible_cast
deleted def unitOfInvertible
added theorem Commute.invOf_left
added theorem Commute.invOf_right
added def Invertible.map
added def Units.invertible
added theorem commute_invOf
added theorem div_self_of_invertible
added theorem invOf_div
added theorem invOf_neg
added theorem invOf_units
added def invertibleDiv
added def invertibleNeg
added theorem isUnit_of_invertible
added theorem map_invOf
added theorem one_sub_invOf_two
added theorem pos_of_invertible_cast
added def unitOfInvertible
added theorem Invertible.congr
added def Invertible.copy'
added def Invertible.copy
added def Invertible.mul
added theorem invOf_eq_group_inv
added theorem invOf_eq_left_inv
added theorem invOf_eq_right_inv
added theorem invOf_inj
added theorem invOf_invOf
added theorem invOf_mul
added theorem invOf_mul_self'
added theorem invOf_mul_self
added theorem invOf_mul_self_assoc'
added theorem invOf_mul_self_assoc
added theorem invOf_one'
added theorem invOf_one
added def invertibleMul
added def invertibleOne
added theorem invertible_unique
added theorem mul_invOf_self'
added theorem mul_invOf_self
added theorem mul_invOf_self_assoc'
added theorem mul_invOf_self_assoc
added theorem invOf_eq_inv
added def invertibleInv
added theorem nonzero_of_invertible