On: Euler's Fizzbuzz (2020)

[edflsafoiewq]

The injection mod15: Z -> Z/15 is an operation and the basic idea here is mod15(pow4(x)) = pow4(mod15(x)), so I think it's correct to call it commutativity.

[vitus → edflsafoiewq]

Well, not quite.

You really want to say that mod15(pow4(x)) == mod15(pow4(mod15(x))).

Example:

(3 ** 4) % 15 = 81 % 15 = 6.

But,

(3 % 15) ** 4 = 3 ** 4 = 81.

(That said, the two functions do commute when you restrict your domain and range to Z/15.)

edit: also, I wouldn't consider mod15 to be an injection, as it's, um, not injective (it maps multiple inputs to the same output).

[edflsafoiewq → vitus]

pow4(mod15(x)) is already in Z/15, you can't apply mod15 to it. The point is pow4ing in Z and then reducing mod 15 is the same as reducing mod 15, then pow4ing in Z/15.

It's not actually the same pow4 on the LHS and RHS (the LHS is in Z, the RHS in Z/15), but I think "commutative" still fits.

> as it's, um, not injective

Er, surjection :)

[vitus → edflsafoiewq]

Well, how about this, if we use pow4' to be modular exponentiation, i.e. mod15 o pow4? (of course then changing mod15 to take Z -> Z so the types line up)

Then the desired statement showing commutativity is

    pow4'(mod15(x)) = pow4'(x) = mod15(pow4'(x))

where that last equality is trivial because

    mod15 o mod15 = mod15

so

    mod15 o pow4' = mod15 o mod15 o pow4 = mod15 o pow4 = pow4'

per associativity of function composition