## Stream: general

### Topic: is_group_hom field name

#### Kevin Buzzard (Mar 18 2019 at 21:02):

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)

(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 (Mar 18 2019 at 21:22):

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

#### Chris Hughes (Mar 19 2019 at 14:20):

I would accept that PR.

Last updated: May 12 2021 at 04:19 UTC