smul/pow_to_lex

Stream: general

[Reid Barton]

These lines from algebra.group.order_synonym are clearly wrong because to_lex_smul and of_lex_smul each occur twice.

@[simp, to_additive to_lex_smul, to_additive_reorder 1 4]
lemma to_lex_pow [has_pow α β] (a : α) (b : β) : to_lex (a ^ b) = to_lex a ^ b := rfl
@[simp, to_additive of_lex_smul, to_additive_reorder 1 4]
lemma of_lex_pow [has_pow α β] (a : lex α) (b : β) : of_lex (a ^ b) = of_lex a ^ b := rfl
@[simp, to_additive to_lex_smul, to_additive_reorder 1 4]
lemma pow_to_lex [has_pow α β] (a : α) (b : β) : a ^ to_lex b = a ^ b := rfl
@[simp, to_additive of_lex_smul, to_additive_reorder 1 4]
lemma pow_of_lex [has_pow α β] (a : α) (b : lex β) : a ^ of_lex b = a ^ b := rfl

[Reid Barton]

I'm not sure exactly what the naming convention is regarding the order of name parts, given that pow and smul take arguments in different orders

[Eric Wieser]

This is maybe a sign that the spelling for "generate a declaration" should be different to "attach an existing one"

[Reid Barton]

Yeah it took me a while to realize that the answer to "what does to_additive do when there is a duplicate name" is "something completely different"

[Yaël Dillies]

Whoops sorry my bad. The last two should be smul_to_lex, smul_of_lex.

[Yaël Dillies]

Oh nevermind, it's more complicated than that :/

[Yaël Dillies]

to_lex_smul'/of_lex_smul' is my best guess