ModEq

Statistics

Metric	Count
Definitions	0
Theorems `modEq_iff_eq_mod_zmultiples`, `not_modEq_iff_ne_mod_zmultiples`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`modEq_iff_eq_mod_zmultiples` 📖	mathematical	—	`ModEq` `toAddCommMonoid` `toAddGroup` `AddSubgroup.zmultiples`	—	`modEq_comm` `AddSubgroup.normal_of_comm`
`not_modEq_iff_ne_mod_zmultiples` 📖	mathematical	—	`ModEq` `toAddCommMonoid`	—	`Iff.not` `modEq_iff_eq_mod_zmultiples`

---