We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
toMap
1 parent 1762356 commit 22f2cfdCopy full SHA for 22f2cfd
1 file changed
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
@@ -415,10 +415,6 @@ abbrev toMonoidHom (f : LocalizationMap S N) : M →* N where
415
__ := f
416
map_one' := f.isLocalizationMap.map_one (f := f.toMulHom)
417
418
-/-- Short for `toMonoidHom`; used to apply a localization map as a function. -/
419
-@[to_additive /-- Short for `toAddMonoidHom`; used to apply a localization map as a function. -/]
420
-abbrev toMap (f : LocalizationMap S N) := f.toMonoidHom
421
-
422
@[to_additive]
423
theorem toMonoidHom_injective : Injective (toMonoidHom : LocalizationMap S N → M →* N) :=
424
fun f g ↦ by cases f; congr! with eq; ext; exact congr($eq _)
0 commit comments