Theorem ProfiniteGrp.ofHom_apply

Modification history

2025-03-14 13:35
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300) …
Modified ProfiniteGrp.ofHom_applyView on Github →
2025-01-31 11:58
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) …
Added ProfiniteGrp.ofHom_applyView on Github →