Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 08:42 391746b1

View on Github →

feat(data/zmod/basic): chinese remainder theorem (#8356)

Estimated changes

Modified src/algebra/char_p/basic.lean

Modified src/algebra/ring/prod.lean

added def ring_equiv.prod_zero_ring

added def ring_equiv.zero_ring_prod

Modified src/data/fintype/basic.lean

added theorem fintype.left_inverse_of_right_inverse_of_card_le

added theorem fintype.right_inverse_of_left_inverse_of_card_le

Modified src/data/int/cast.lean

added theorem prod.fst_int_cast

added theorem prod.snd_int_cast

Modified src/data/nat/cast.lean

added theorem prod.fst_nat_cast

added theorem prod.snd_nat_cast

Modified src/data/nat/gcd.lean

added theorem nat.coprime.eq_of_mul_eq_zero

added theorem nat.lcm_dvd_iff

Modified src/data/zmod/basic.lean

added theorem prod.fst_zmod_cast

added theorem prod.snd_zmod_cast

modified theorem zmod.card

added def zmod.chinese_remainder