Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-04 14:28 c2e78d27

View on Github →

refactor(data/zmod): generalize zmod.cast_hom (#2900) Currently, zmod.cast_hom would cast zmod n to rings R of characteristic n. This PR builds cast_hom for rings R with characteristic m that divides n.

Estimated changes

added theorem zmod.cast_add'
modified theorem zmod.cast_add
modified def zmod.cast_hom
modified theorem zmod.cast_hom_apply
added theorem zmod.cast_int_cast'
modified theorem zmod.cast_int_cast
added theorem zmod.cast_mul'
modified theorem zmod.cast_mul
added theorem zmod.cast_nat_cast'
modified theorem zmod.cast_nat_cast
added theorem zmod.cast_one'
modified theorem zmod.cast_one
added theorem zmod.cast_pow'
added theorem zmod.cast_pow
added theorem zmod.cast_sub'
added theorem zmod.cast_sub