Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-16 11:34 844a4f7b

View on Github →

refactor(algebra/hom/group): Generalize map_inv to division monoids (#14134) A minor change with unexpected instance synthesis breakage. A good deal of dot notation on monoid_hom.map_inv breaks, along with a few uses of map_inv. Expliciting the type fixes them all, but this is still quite concerning.

Estimated changes

modified theorem map_div'
modified theorem map_div
modified theorem map_inv
modified theorem map_mul_inv
modified theorem map_zpow
modified theorem map_zsmul