Commit 2023-10-02 06:27 465105ce

View on Github →

feat: some lemmas about List and ZMod (#7424)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.drop_tail

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.cast_injective_of_lt

added theorem ZMod.cast_zmod_eq_zero_iff_of_lt

added theorem ZMod.val_add_le

added theorem ZMod.val_add_of_le

added theorem ZMod.val_add_of_lt

added theorem ZMod.val_add_val_of_le

added theorem ZMod.val_cast_eq_val_of_lt

modified theorem ZMod.val_injective

added theorem ZMod.val_mul_le

added theorem ZMod.val_mul_of_lt

added theorem ZMod.val_nat_cast_of_lt

added theorem ZMod.val_ne_zero

added theorem ZMod.val_neg_of_ne_zero

added theorem ZMod.val_sub

Modified Mathlib/Logic/Basic.lean

added theorem dite_prop_iff_and

added theorem dite_prop_iff_or

added theorem ite_prop_iff_and

added theorem ite_prop_iff_or