has_pow_of_has_one_has_mul

Stream: Is there code for X?

[Joseph Hua]

I made this because I don't have a monoid but need to express powers:

/-- More general version of monoid.has_pow -/
instance has_pow_of_has_one_has_mul (A : Type*) [has_one A] [has_mul A] :
  has_pow A ℕ := ⟨ λ t k, npow_rec k t ⟩

However, if I have a monoid this is going to confuse with the instance of the original monoid.has_has? Currently I'm trying to prove something and it's basically asking me to show that

lemma comeone {A : Type*} [monoid A] :
  monoid.has_pow = has_pow_of_has_one_has_mul A :=
sorry

Is this kind of thing already dealt with / why does the definition of monoid mention pow at all?

[Anne Baanen]

Isn't there already something called docs#npow_rec?

[Anne Baanen]

The reason monoid contains pow is because otherwise we'd get distinct module ℕ ℕ structures:

[Joseph Hua]

Anne Baanen said:

The reason monoid contains pow is because otherwise we'd get distinct module ℕ ℕ structures:

yes I used npow_rec in my definition. Are you saying that having this more general has_pow has an instance is just a bad idea?

[Anne Baanen]

There are two ways that the natural numbers are an ℕ-semimodule: all additive monoids are ℕ-semimodules by defining recursively 0 • x = 0 and (n+1) • x = n • x + x. And all semirings are modules over themselves by defining x • y = x * y. Now for whatever reason, multiplication of natural numbers is defined by recursion on the parameter on the right, so the two definitions of scalar multiplication don't line up. (Even though you can prove them to return equal values, the definitions do not look the same.)

In general, you need all instances to have the same definition, and the solution chosen in mathlib is to include the definition of nsmul, scalar multiplication by a natural, into the add_monoid class.

[Anne Baanen]

Since add_monoid is defined as a copy of monoid with multiplicative terms replaced with additive terms, you need to add the corresponding npow field to monoid.

[Anne Baanen]

So the conclusion is: you should be able to prove that exponentiation of monoids is equal to npow_rec, or your instance, you cannot define this to be the case because it will make the library as a whole incoherent.

[Joseph Hua]

I see! Thank you :)

[Anne Baanen]

You're welcome! It's a complicated story that the Mathlib community only figured out this year (#7084), so you definitely deserve an explanation :)

[Anne Baanen]

I just saw the expression "anecdotal defeq" in that PR, which I'm definitely adding to my vocabulary :D

[Eric Wieser]

I made this because I don't have a monoid but need to express powers:

Do you have a mul_one_class?

[Joseph Hua]

Eric Wieser said:

I made this because I don't have a monoid but need to express powers:

Do you have a mul_one_class?

i only have has_one and has_mul