Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 01:29 649ca66b

View on Github →

chore(*): Disparate generalizations to division monoids (#14686) The leftover changes from the introduction of division_monoid.

Estimated changes

modified theorem commute.inv_inv
modified theorem commute.inv_inv_iff
modified def div_monoid_hom
modified theorem semiconj_by.inv_inv_symm
deleted theorem commute.inv_inv₀
deleted theorem units.coe_inv'
deleted theorem units.coe_zpow₀
modified def arrow_action