ModEq

📁 Source: Mathlib/Algebra/Group/ModEq.lean

Statistics

Metric	Count
Definitions `«term_≡_[PMOD_]»`	1
Theorems `add`, `add_iff_left`, `add_iff_right`, `add_left`, `add_left_cancel`, `add_left_cancel'`, `add_nsmul`, `add_right`, `add_right_cancel`, `add_right_cancel'`, `add_zsmul`, `map`, `neg`, `neg'`, `nsmul`, `nsmul_add`, `nsmul_cancel`, `nsmul_cases`, `of_neg`, `of_neg'`, `of_nsmul`, `of_zsmul`, `sub`, `sub_iff_left`, `sub_iff_right`, `sub_left`, `sub_left_cancel`, `sub_left_cancel'`, `sub_right`, `sub_right_cancel`, `sub_right_cancel'`, `trans`, `zsmul`, `zsmul_add`, `zsmul_cancel`, `add_modEq_left`, `add_modEq_right`, `add_nsmul_modEq`, `add_zsmul_modEq`, `instIsTransModEq`, `instReflModEq`, `instSymmModEq`, `map_modEq_iff`, `modEq_comm`, `modEq_iff_eq_add_zsmul`, `modEq_iff_nsmul`, `modEq_iff_zsmul`, `modEq_iff_zsmul'`, `modEq_neg`, `modEq_nsmul_cases`, `modEq_refl`, `modEq_rfl`, `modEq_sub`, `modEq_sub_iff_add_modEq`, `modEq_sub_iff_add_modEq'`, `modEq_zero`, `modEq_zero_iff_eq_zsmul`, `neg_modEq_neg`, `not_modEq_iff_ne_add_zsmul`, `nsmul_add_modEq`, `nsmul_modEq_nsmul`, `self_modEq_zero`, `sub_modEq_iff_modEq_add`, `sub_modEq_iff_modEq_add'`, `sub_modEq_zero`, `zsmul_add_modEq`, `zsmul_modEq_zero`, `zsmul_modEq_zsmul`	68
Total	69

AddCommGroup

Definitions

Name	Category	Theorems
`«term_≡_[PMOD_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_modEq_left` 📖	mathematical	—	`ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`add_zero` `ModEq.add_iff_left` `modEq_refl`
`add_modEq_right` 📖	mathematical	—	`ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`add_comm`
`add_nsmul_modEq` 📖	mathematical	—	`ModEq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`modEq_iff_nsmul` `zero_nsmul` `add_comm` `add_zero`
`add_zsmul_modEq` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`modEq_iff_zsmul` `neg_zsmul` `sub_add_cancel_left`
`instIsTransModEq` 📖	mathematical	—	`IsTrans` `ModEq`	—	`ModEq.trans`
`instReflModEq` 📖	mathematical	—	`ModEq`	—	`modEq_refl`
`instSymmModEq` 📖	mathematical	—	`ModEq`	—	`ModEq.symm`
`map_modEq_iff` 📖	mathematical	`DFunLike.coe`	`ModEq`	—	`AddMonoidHomClass.toAddHomClass`
`modEq_comm` 📖	mathematical	—	`ModEq`	—	`ModEq.symm`
`modEq_iff_eq_add_zsmul` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup`	—	—
`modEq_iff_nsmul` 📖	mathematical	—	`ModEq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—
`modEq_iff_zsmul` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup` `SubNegMonoid.toSub`	—	`modEq_iff_nsmul` `sub_zsmul` `sub_eq_add_neg` `sub_eq_sub_iff_add_eq_add` `add_comm` `natCast_zsmul`
`modEq_iff_zsmul'` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `SubNegMonoid.toZSMul`	—	—
`modEq_neg` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`modEq_comm` `zsmul_neg'` `neg_zsmul` `neg_sub`
`modEq_nsmul_cases` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_comm` `sub_right_comm` `sub_eq_iff_eq_add`
`modEq_refl` 📖	mathematical	—	`ModEq`	—	`zero_nsmul` `zero_add`
`modEq_rfl` 📖	mathematical	—	`ModEq`	—	`modEq_refl`
`modEq_sub` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`one_nsmul` `sub_add_cancel` `zero_nsmul` `zero_add`
`modEq_sub_iff_add_modEq` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_sub_iff_add_modEq'` `add_comm`
`modEq_sub_iff_add_modEq'` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`sub_sub`
`modEq_zero` 📖	mathematical	—	`ModEq` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`nsmul_zero` `zero_add`
`modEq_zero_iff_eq_zsmul` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `SubNegMonoid.toZSMul`	—	`modEq_comm` `modEq_iff_eq_add_zsmul` `zero_add`
`neg_modEq_neg` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`modEq_comm` `sub_neg_eq_add` `neg_add_eq_sub`
`not_modEq_iff_ne_add_zsmul` 📖	mathematical	—	`ModEq` `toAddCommMonoid`	—	`modEq_iff_eq_add_zsmul`
`nsmul_add_modEq` 📖	mathematical	—	`ModEq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`modEq_iff_nsmul` `zero_nsmul` `zero_add`
`nsmul_modEq_nsmul` 📖	mathematical	—	`ModEq` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`mul_nsmul` `mul_nsmul'`
`self_modEq_zero` 📖	mathematical	—	`ModEq` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`modEq_iff_nsmul` `zero_nsmul` `zero_add` `one_nsmul` `add_zero`
`sub_modEq_iff_modEq_add` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_comm` `modEq_sub_iff_add_modEq`
`sub_modEq_iff_modEq_add'` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_comm` `modEq_sub_iff_add_modEq'`
`sub_modEq_zero` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`zero_add`
`zsmul_add_modEq` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`modEq_iff_zsmul` `neg_zsmul` `sub_add_cancel_right`
`zsmul_modEq_zero` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`modEq_iff_zsmul` `neg_zsmul` `zero_sub`
`zsmul_modEq_zsmul` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `toAddGroup`	—	`zsmul_comm`

AddCommGroup.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`AddCommGroup.ModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`AddCommGroup.modEq_iff_nsmul` `add_nsmul` `add_add_add_comm`
`add_iff_left` 📖	mathematical	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`AddCommGroup.modEq_iff_nsmul` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `add_assoc` `add_comm` `add_nsmul` `add_right_comm` `add_add_add_comm` `add`
`add_iff_right` 📖	mathematical	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_comm` `add_iff_left`
`add_left` 📖	mathematical	`AddCommGroup.ModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add` `AddCommGroup.modEq_rfl`
`add_left_cancel` 📖	—	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_iff_left`
`add_left_cancel'` 📖	—	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_left_cancel` `AddCommGroup.modEq_rfl`
`add_nsmul` 📖	mathematical	`AddCommGroup.ModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`trans` `AddCommGroup.add_nsmul_modEq`
`add_right` 📖	mathematical	`AddCommGroup.ModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add` `AddCommGroup.modEq_rfl`
`add_right_cancel` 📖	—	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_iff_right`
`add_right_cancel'` 📖	—	`AddCommGroup.ModEq` `AddCancelCommMonoid.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_right_cancel` `AddCommGroup.modEq_rfl`
`add_zsmul` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`trans` `AddCommGroup.add_zsmul_modEq`
`map` 📖	mathematical	`AddCommGroup.ModEq`	`DFunLike.coe`	—	`AddCommGroup.modEq_iff_nsmul` `map_add` `AddMonoidHomClass.toAddHomClass` `map_nsmul`
`neg` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`AddCommGroup.neg_modEq_neg`
`neg'` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`AddCommGroup.modEq_neg`
`nsmul` 📖	mathematical	`AddCommGroup.ModEq`	`AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`AddCommGroup.modEq_iff_nsmul` `mul_nsmul` `mul_nsmul'` `nsmul_add`
`nsmul_add` 📖	mathematical	`AddCommGroup.ModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`trans` `AddCommGroup.nsmul_add_modEq`
`nsmul_cancel` 📖	—	`AddCommGroup.ModEq` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—	`AddCommGroup.nsmul_modEq_nsmul`
`nsmul_cases` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`AddCommGroup.modEq_nsmul_cases`
`of_neg` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`AddCommGroup.neg_modEq_neg`
`of_neg'` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`AddCommGroup.modEq_neg`
`of_nsmul` 📖	—	`AddCommGroup.ModEq` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—	`mul_nsmul'`
`of_zsmul` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`AddCommGroup.modEq_iff_zsmul`
`sub` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_iff_left`
`sub_iff_left` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg`
`sub_iff_right` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg`
`sub_left` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub` `AddCommGroup.modEq_rfl`
`sub_left_cancel` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`sub_iff_left`
`sub_left_cancel'` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`sub_left_cancel` `AddCommGroup.modEq_rfl`
`sub_right` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub` `AddCommGroup.modEq_rfl`
`sub_right_cancel` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`sub_iff_right`
`sub_right_cancel'` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`sub_right_cancel` `AddCommGroup.modEq_rfl`
`trans` 📖	—	`AddCommGroup.ModEq`	—	—	`AddCommGroup.modEq_iff_nsmul` `add_nsmul` `add_assoc` `add_left_comm`
`zsmul` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`AddCommGroup.modEq_iff_zsmul` `zsmul_sub` `mul_zsmul` `mul_zsmul'`
`zsmul_add` 📖	mathematical	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`trans` `AddCommGroup.zsmul_add_modEq`
`zsmul_cancel` 📖	—	`AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—	`AddCommGroup.zsmul_modEq_zsmul`

---

← Back to Index