Theorem OneHom.mul_apply

Modification history

2026-11-10 14:10

Mathlib/Algebra/Group/Hom/Basic.lean

feat: use `IsApply` for `OneHom` (#45472)

Deleted OneHom.mul_apply View on Github →

2025-09-06 10:02

Mathlib/Algebra/Group/Hom/Basic.lean

feat: instances for `ZeroHom` and `OneHom` (#27305) …

Added OneHom.mul_apply View on Github →