Mathlib v3 is deprecated. Go to Mathlib v4

Def monoid_hom.to_localization_map

Modification history

2020-05-16 21:18

src/group_theory/monoid_localization.lean

refactor(group_theory/monoid_localization): use old_structure_cmd (#2683) …

Added monoid_hom.to_localization_map View on Github →