Zulip Chat Archive

Stream: general

Topic: duplicate lemmas

Eric Wieser (Mar 06 2022 at 11:34):

Which should we keep? (docs#multiset.prod_le_pow_card, docs#multiset.pow_card_le_prod) or docs#multiset.prod_le_of_forall_le?

cc @Joachim Breitner, since you're renaming the latter in #12473

Yaël Dillies (Mar 06 2022 at 11:37):

The latter, to match docs#finset.prod_le_of_forall_le and docs#finset.le_prod_of_forall_le.

Eric Wieser (Mar 06 2022 at 11:39):

Obviously if we keep the former, we'd rename the finset lemmas

Joachim Breitner (Mar 06 2022 at 11:42):

I like the former more (mention more of the symbols in the conclusion of the lemma, namely card)

Joachim Breitner (Mar 07 2022 at 09:28):

Do we have a decision here? Should I do this before #12473 can land, or can we do the cleanup afterwards (to avoid putting the critical path to finite group nilpotency theorem through more rabbit holes :-))

Eric Wieser (Mar 07 2022 at 13:27):

/poll Which style of name is better

  • prod_le_of_forall_le
  • prod_le_pow_card
  • prod_le_pow_card_of_forall_le

Johan Commelin (Mar 11 2022 at 10:13):

@Joachim Breitner I think prod_le_pow_card is the winner.

Joachim Breitner (Mar 11 2022 at 10:59):

I’m on it (in #12589)

Eric Wieser (May 21 2022 at 13:02):

/poll Which should we keep

  • equiv.set.of_eq
  • equiv.set_congr

Eric Wieser (May 21 2022 at 13:03):

docs#equiv.set.of_eq, docs#equiv.set_congr. Both are (h : s = t) : ↥s ≃ ↥t.

Not to be confused with docs#equiv.set.congr which is (e : α ≃ β) : set α ≃ set β and matches docs#equiv.finset_congr.

Eric Wieser (May 21 2022 at 13:04):

Note we have docs#linear_equiv.of_eq but docs#add_equiv.add_subgroup_congr.

Eric Wieser (May 21 2022 at 13:04):

cc @Anatole Dedecker, who ended up trying to PR a missing one of these in #14267 because the two different naming styles led them astray.

Anatole Dedecker (May 21 2022 at 13:05):

Indeed :sweat_smile:

Eric Wieser (May 21 2022 at 13:23):

@Yaël Dillies, does your set.coe_congr suggestion indicate we should rename add_equiv.add_subgroup_congr to add_subgroup.coe_congr and linear_equiv.of_eq to submodule.coe_congr?

Yaël Dillies (May 21 2022 at 13:24):

Yes, I think so.

Yaël Dillies (May 21 2022 at 13:25):

or just .congr instead of .coe_congr. I'm just unsure whether set.congr would be a reasonable name.

Eric Wieser (May 21 2022 at 13:26):

Or the longer coe_sort_congr

Yaël Dillies (May 21 2022 at 13:26):

That would clear up ambiguities.

Eric Wieser (May 21 2022 at 13:26):

Is it a problem that the type of the equiv is no longer in the name?

Yaël Dillies (May 21 2022 at 13:27):

Depends. Does it ever happen that we can decorate the equiv in different ways?

Eric Wieser (May 21 2022 at 13:27):

The equivalence between equal add_subgroups could be int-linear, but really that's two steps

Eric Wieser (May 21 2022 at 13:28):

Ah, here's an answer; with the new docs#add_submonoid_class it's possible to get an add_equiv between submodules

Eric Wieser (May 21 2022 at 13:28):

Which you would not expect to have to look for in the add_submonoid namespace.

Last updated: Aug 03 2023 at 10:10 UTC