## Stream: general

### Topic: is_group_hom.mul

#### Kenny Lau (Apr 12 2018 at 05:54):

This is what is_group_hom.mul looked like on Apr 5:

namespace is_group_hom
variables {f : α → β} (H : is_group_hom f)
include H

theorem mul : ∀ a b : α, f (a * b) = f a * f b := H


Now, the function variable became explicit, which broke some of my files. Are changes like this just going to happen randomly without any notice?

wonderful

#### Mario Carneiro (Apr 12 2018 at 05:56):

mathlib is not stable any more than lean itself is, be prepared for this sort of thing

#### Kenny Lau (Apr 12 2018 at 05:56):

https://github.com/leanprover/mathlib/commit/fa86d349527766c2d0fc3173fcda302cdd5673f3#diff-52b9e281e7667f88f8203fb617843d93L488

#### Mario Carneiro (Apr 12 2018 at 05:56):

It's not clear what kind of notice would be appropriate here in any case

#### Kenny Lau (Apr 12 2018 at 05:57):

so if i werent clever enough to know exactly that my files broke because they made this variable explicit, I'm just going to have to sit down for an hour?

#### Kenny Lau (Apr 12 2018 at 05:58):

also, this change broke h.one where h is the proof that some function is a group homomorphism

#### Kenny Lau (Apr 12 2018 at 05:58):

now I have to do is_group_hom.one _ h

#### Mario Carneiro (Apr 12 2018 at 05:58):

If you update and your files break, double check what changed in the update, should give you a hint at what to do

#### Mario Carneiro (Apr 12 2018 at 05:58):

Now you do is_group_hom.one f I think

right

#### Kenny Lau (Apr 12 2018 at 06:00):

suddenly is_group_hom became a class

and guess what

#### Kenny Lau (Apr 12 2018 at 06:00):

https://github.com/leanprover/mathlib/commit/fa86d349527766c2d0fc3173fcda302cdd5673f3#diff-52b9e281e7667f88f8203fb617843d93L515

#### Mario Carneiro (Apr 12 2018 at 06:00):

Complain to @Scott Morrison and @Johannes Hölzl, I think this change is still in its probationary period

#### Kenny Lau (Apr 12 2018 at 06:01):

before: theorem inv (a : α) : (f a)⁻¹ = f a⁻¹
after: theorem inv (a : α) : f a⁻¹ = (f a)⁻¹

really

#### Mario Carneiro (Apr 12 2018 at 06:01):

I agree with that change, it makes more sense the other way around to match with one and mul

#### Mario Carneiro (Apr 12 2018 at 06:03):

but one thing I will not do is avoid small consistency changes because of a worry of breaking things. Once you start doing that, it will only become more crufty as time goes on

Last updated: May 11 2021 at 23:11 UTC