Commit 2022-12-10 13:15 6bd866ef

View on Github →

feat port: Algebra.Invertible (#930) 10b4e499f43088dd3bb7b5796184ad5216648ab1 I had to import norm_num and generalize some proofs in another file from Semiring to NonAssocSemiring.

Estimated changes

added theorem Commute.invOf_left
added theorem Commute.invOf_right
added def Invertible.copy
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_eq_group_inv
added theorem invOf_eq_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_assoc
added theorem invOf_neg
added theorem invOf_one
added theorem invOf_units
added def invertibleDiv
added def invertibleInv
added def invertibleMul
added def invertibleNeg
added def invertibleOne
added theorem invertible_unique
added theorem isUnit_of_invertible
added theorem map_invOf
added theorem mul_invOf_self
added theorem mul_invOf_self_assoc
added theorem nonzero_of_invertible
added theorem one_sub_invOf_two
added def unitOfInvertible