is_group_hom field name

Stream: general

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/e8bdc7fc14c6d56d4040892d16929f310e9d03d5/src/algebra/group.lean#L627

says TODO rename fields of is_group_hom: mul ↝ map_mul?. Hey, cool squiggly arrow Scott. @Chris Hughes @Mario Carneiro that looks like a sensible change to me. Would a PR making the change be welcomed?

class is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) : Prop :=
(map_one : f 1 = 1)
(map_mul : ∀ {x y}, f (x * y) = f x * f y)
(map_add : ∀ {x y}, f (x + y) = f x + f y)

class is_monoid_hom [monoid α] [monoid β] (f : α → β) : Prop :=
(map_one : f 1 = 1)
(map_mul : ∀ {x y}, f (x * y) = f x * f y)

class is_add_monoid_hom [add_monoid α] [add_monoid β] (f : α → β) : Prop :=
(map_zero : f 0 = 0)
(map_add : ∀ {x y}, f (x + y) = f x + f y)

but

class is_group_hom [group α] [group β] (f : α → β) : Prop :=
(mul : ∀ a b : α, f (a * b) = f a * f b)

[Patrick Massot]

Did you study applications of these axioms? Does it read weird? I guess using bundled maps everywhere would make clearer here...

[Chris Hughes]

I would accept that PR.