## Stream: maths

### Topic: nat.mod_mul_mod

#### Kevin Buzzard (Mar 05 2020 at 19:42):

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 (Mar 05 2020 at 21:22):

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 (Mar 06 2020 at 07:42):

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 (Mar 06 2020 at 07:47):

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

#### Johan Commelin (Mar 06 2020 at 07:48):

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

#### Kevin Buzzard (Mar 06 2020 at 08:59):

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

Last updated: May 11 2021 at 16:22 UTC