Commit 2023-05-12 14:43 b29921cb

View on Github →

feat: port Algebra.Modeq (#3921)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

modified theorem Int.cast_mul_eq_zsmul_cast

Created Mathlib/Algebra/ModEq.lean

added theorem AddCommGroup.ModEq.trans

added def AddCommGroup.ModEq

added theorem AddCommGroup.add_modEq_left

added theorem AddCommGroup.add_modEq_right

added theorem AddCommGroup.add_nsmul_modEq

added theorem AddCommGroup.add_zsmul_modEq

added theorem AddCommGroup.int_cast_modEq_int_cast

added theorem AddCommGroup.modEq_comm

added theorem AddCommGroup.modEq_iff_eq_add_zsmul

added theorem AddCommGroup.modEq_iff_eq_mod_zmultiples

added theorem AddCommGroup.modEq_iff_int_modEq

added theorem AddCommGroup.modEq_neg

added theorem AddCommGroup.modEq_refl

added theorem AddCommGroup.modEq_rfl

added theorem AddCommGroup.modEq_sub

added theorem AddCommGroup.modEq_sub_iff_add_modEq'

added theorem AddCommGroup.modEq_sub_iff_add_modEq

added theorem AddCommGroup.modEq_zero

added theorem AddCommGroup.nat_cast_modEq_nat_cast

added theorem AddCommGroup.neg_modEq_neg

added theorem AddCommGroup.not_modEq_iff_ne_add_zsmul

added theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples

added theorem AddCommGroup.nsmul_add_modEq

added theorem AddCommGroup.nsmul_modEq_nsmul

added theorem AddCommGroup.self_modEq_zero

added theorem AddCommGroup.sub_modEq_iff_modEq_add'

added theorem AddCommGroup.sub_modEq_iff_modEq_add

added theorem AddCommGroup.sub_modEq_zero

added theorem AddCommGroup.zsmul_add_modEq

added theorem AddCommGroup.zsmul_modEq_zero

added theorem AddCommGroup.zsmul_modEq_zsmul