Commit 2021-10-29 17:12 c5456607

View on Github →

chore(algebra/group_with_zero/basic): move ring.inverse, generalize and rename inverse_eq_has_inv (#10033) This moves ring.inverse earlier in the import graph, since it's not about rings at all.

Estimated changes

Modified src/algebra/field.lean

deleted theorem inverse_eq_has_inv

Modified src/algebra/group_with_zero/basic.lean

added theorem ring.inverse_eq_inv'

added theorem ring.inverse_eq_inv

added theorem ring.inverse_mul_cancel

added theorem ring.inverse_mul_cancel_left

added theorem ring.inverse_mul_cancel_right

added theorem ring.inverse_non_unit

added theorem ring.inverse_unit

added theorem ring.mul_inverse_cancel

added theorem ring.mul_inverse_cancel_left

added theorem ring.mul_inverse_cancel_right

added theorem ring.mul_inverse_rev

Modified src/algebra/ring/basic.lean

deleted theorem ring.inverse_mul_cancel

deleted theorem ring.inverse_mul_cancel_left

deleted theorem ring.inverse_mul_cancel_right

deleted theorem ring.inverse_non_unit

deleted theorem ring.inverse_unit

deleted theorem ring.mul_inverse_cancel

deleted theorem ring.mul_inverse_cancel_left

deleted theorem ring.mul_inverse_cancel_right

deleted theorem ring.mul_inverse_rev

Modified src/analysis/calculus/times_cont_diff.lean