duplicate lemmas

Stream: general

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Joachim Breitner]

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

[Joachim Breitner]

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]

/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]

@Joachim Breitner I think prod_le_pow_card is the winner.

[Joachim Breitner]

I’m on it (in #12589)

[Eric Wieser]

/poll Which should we keep

• equiv.set.of_eq
• equiv.set_congr

[Eric Wieser]

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]

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

[Eric Wieser]

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]

Indeed :sweat_smile:

[Eric Wieser]

@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]

Yes, I think so.

[Yaël Dillies]

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

[Eric Wieser]

Or the longer coe_sort_congr

[Yaël Dillies]

That would clear up ambiguities.

[Eric Wieser]

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

[Yaël Dillies]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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