Commit 2024-07-24 14:17 b0acd6e2

View on Github →

feat(ZMod): Simple lemmas (#15076) From LeanAPAP

Estimated changes

Modified Mathlib/Data/ZMod/Basic.lean

modified theorem ZMod.coe_intCast

added theorem ZMod.intCast_cast_add

added theorem ZMod.intCast_cast_mul

added theorem ZMod.intCast_cast_neg

added theorem ZMod.intCast_cast_sub

added theorem ZMod.lift_injective

added theorem ZMod.mul_val_inv

added theorem ZMod.val_inv_mul

added theorem ZMod.val_one''

added theorem nsmul_zmod_val_inv_nsmul

added theorem pow_pow_zmod_val_inv

added theorem pow_zmod_val_inv_pow

added theorem zmod_val_inv_nsmul_nsmul