Theorem MulHom.prod_map_comap_prod'

Modification history

2023-08-10 19:52

Mathlib/GroupTheory/Subsemigroup/Operations.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified MulHom.prod_map_comap_prod'View on Github →

2022-12-31 09:21

Mathlib/GroupTheory/Subsemigroup/Operations.lean

feat: port GroupTheory.Subsemigroup.Operations (#1235)

Added MulHom.prod_map_comap_prod'View on Github →