Def MonoidHom.restrictHom

Modification history

2026-07-20 01:34

Mathlib/Algebra/Group/Submonoid/Operations.lean

refactor: rename restrict to domRestrict (#25980) …

Deleted MonoidHom.restrictHom View on Github →

2026-02-13 16:28

Mathlib/Algebra/Group/Submonoid/Operations.lean

feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective (#33403) …

Added MonoidHom.restrictHom View on Github →