ModEq

Statistics

Metric	Count
Definitions	0
Theorems `div_modEq_div`, `mul_modEq_mul_left`, `mul_modEq_mul_right`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`div_modEq_div` 📖	mathematical	—	`ModEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`nsmul_eq_mul` `add_div'` `mul_assoc` `div_left_inj'`
`mul_modEq_mul_left` 📖	mathematical	—	`ModEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`mul_comm`
`mul_modEq_mul_right` 📖	mathematical	—	`ModEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_eq_mul_inv` `div_modEq_div` `inv_ne_zero` `div_inv_eq_mul`

---