nat.mod_mul_mod

Stream: maths

[Kevin Buzzard]

example (a b c : ℕ) : ((a % c) * (b % c)) % c = (a * b) % c := sorry :-/ I can't find this in the library. Is it called mod_mul_cast or something?

[Kevin Buzzard]

theorem mod_mul_mod_mod_eq_mul_mod (a b c : ℕ) : ((a % c) * (b % c)) % c = (a * b) % c :=
nat.modeq.modeq_mul (nat.modeq.mod_modeq a c) (nat.modeq.mod_modeq b c)

Now all it needs is a sensible name :-)

[Patrick Stevens]

Kevin Buzzard said:

theorem mod_mul_mod_mod_eq_mul_mod (a b c : ℕ) : ((a % c) * (b % c)) % c = (a * b) % c :=
nat.modeq.modeq_mul (nat.modeq.mod_modeq a c) (nat.modeq.mod_modeq b c)

Now all it needs is a sensible name :-)

It's basically "* is a semiring homomorpism from N to Z_n", right?

[Kevin Buzzard]

In some form. One could argue that that was what modeq_mul was

[Johan Commelin]

It's basically "% c is a monoid hom from N to Z_c".

[Kevin Buzzard]

In some form. It's just one of those situations where there is more than one way of saying something and I needed a way which wasn't in the library