Commit 2023-03-23 19:08 d37b34f1

View on Github →

feat: commute/div lemmas (#3055) Match https://github.com/leanprover-community/mathlib/pull/18607

Estimated changes

modified theorem inv_add_inv
modified theorem one_div_add_one_div
deleted theorem Commute.inv_inv
modified theorem Commute.cast_int_left
modified theorem Commute.cast_int_right
modified theorem Commute.cast_nat_mul_self
modified theorem Commute.self_cast_nat_mul