Zulip Chat Archive

Stream: new members

Topic: Control `to_additive`

Pedro Minicz (Jun 13 2020 at 19:19):

How can I tell to_additive to ignore some definitions?

Pedro Minicz (Jun 13 2020 at 19:19):

import group_theory.quotient_group
import set_theory.ordinal

open quotient_group

namespace cardinal

variables {α : Type*} [group α] {s : set α} [is_subgroup s]

@[to_additive]
lemma mk_group_eq_mk_quotient_mul_mk_subgroup :
  mk α = mk (quotient s) * mk s :=
begin
  rw [mul_def, cardinal.eq],
  exact ⟨is_subgroup.group_equiv_quotient_times_subgroup _⟩
end

Johan Commelin (Jun 13 2020 at 19:20):

What should it ignore?

Kevin Buzzard (Jun 13 2020 at 19:20):

What's the problem?

Johan Commelin (Jun 13 2020 at 19:20):

The *?

Pedro Minicz (Jun 13 2020 at 19:20):

I am pretty sure that the problem in the example above is that to_additive changes * to +.

Kevin Buzzard (Jun 13 2020 at 19:21):

oh yeah :-)

Pedro Minicz (Jun 13 2020 at 19:21):

The lemma is true for both group and add_group, but the cardinals should always be multiplied!

Johan Commelin (Jun 13 2020 at 19:21):

I guess that in this case you will have to restate the lemma, but you can prove it using multiplicate A for the additive group A.

Johan Commelin (Jun 13 2020 at 19:21):

So the proof of the additive version will be a one-liner, reusing the multiplicative one.

Johan Commelin (Jun 13 2020 at 19:21):

Hopefully that works.

Pedro Minicz (Jun 13 2020 at 19:21):

Also, I could be that its changing mul_def to add_def, maybe.

Johan Commelin (Jun 13 2020 at 19:22):

Probably

Pedro Minicz (Jun 13 2020 at 19:22):

The error message is quite weird, it complains about @has_add.add cardinal cardinal.has_mul.

Pedro Minicz (Jun 13 2020 at 19:27):

@Johan Commelin could you give a mwe for multiplicate, I don't seem to be able to find it on the docs.

Kevin Buzzard (Jun 13 2020 at 19:27):

multiplicative

Johan Commelin (Jun 13 2020 at 19:28):

git grep multiplicative will give you a lot of examples

Johan Commelin (Jun 13 2020 at 19:29):

@Pedro Minicz For example: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/big_operators.lean#L533

Patrick Massot (Jun 13 2020 at 19:46):

Pedro, it's nice to move away from the thread whose name shall not be written, but actually you could take the next step. This discussion could be in the general stream. This is clearly not a new member question.

Pedro Minicz (Jun 13 2020 at 19:58):

Okay, can I move this thread?

Pedro Minicz (Jun 13 2020 at 19:59):

Well, I will make another thread. If there is a way to move them please teach me and I'll keep it in mind.

Kevin Buzzard (Jun 13 2020 at 20:00):

You got a promotion :-) I think that if you started the topic then you might be able to change it. There are people like Yury who wrote to_additive and who might not read the new members stream at all.

Patrick Massot (Jun 13 2020 at 20:02):

Only admins can move a topic to another stream.

Last updated: Dec 20 2023 at 11:08 UTC