Division

📁 Source: Mathlib/Algebra/MonoidAlgebra/Division.lean

Statistics

Metric	Count
Definitions `divOf`, `divOfHom`, `modOf`	3
Theorems `add_divOf`, `divOfHom_apply_apply`, `divOf_add`, `divOf_add_modOf`, `divOf_apply`, `divOf_zero`, `modOf_add_divOf`, `modOf_apply_add_self`, `modOf_apply_of_exists_add`, `modOf_apply_of_not_exists_add`, `modOf_apply_self_add`, `mul_of'_divOf`, `mul_of'_modOf`, `of'_divOf`, `of'_dvd_iff_modOf_eq_zero`, `of'_modOf`, `of'_mul_divOf`, `of'_mul_modOf`, `support_divOf`, `zero_divOf`	20
Total	23

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`divOf` 📖	CompOp	12 math math: `zero_divOf`, `of'_divOf`, `divOf_add`, `divOfHom_apply_apply`, `divOf_apply`, `divOf_zero`, `of'_mul_divOf`, `add_divOf`, `modOf_add_divOf`, `support_divOf`, `divOf_add_modOf`, `mul_of'_divOf`
`divOfHom` 📖	CompOp	1 math math: `divOfHom_apply_apply`
`modOf` 📖	CompOp	10 math math: `modOf_apply_add_self`, `modOf_apply_of_not_exists_add`, `of'_dvd_iff_modOf_eq_zero`, `modOf_apply_of_exists_add`, `mul_of'_modOf`, `modOf_add_divOf`, `modOf_apply_self_add`, `divOf_add_modOf`, `of'_mul_modOf`, `of'_modOf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_divOf` 📖	mathematical	—	`divOf` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`divOfHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `nonAssocSemiring` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `MonoidHom` `Multiplicative` `AddMonoid.End` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AddMonoid.End.instSemiring` `addAddCommMonoid` `MonoidHom.instFunLike` `divOfHom` `divOf` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`divOf_add` 📖	mathematical	—	`divOf` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`ext` `add_assoc`
`divOf_add_modOf` 📖	mathematical	—	`AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instMul` `of'` `divOf` `modOf`	—	`ext` `Finsupp.add_apply` `em` `modOf_apply_self_add` `add_zero` `of'_apply` `single_mul_apply_aux` `IsCancelAdd.toIsLeftCancelAdd` `one_mul` `divOf_apply` `modOf_apply_of_not_exists_add` `single_mul_apply_of_not_exists_add` `zero_add`
`divOf_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `divOf` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`divOf_zero` 📖	mathematical	—	`divOf` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`ext` `zero_add`
`modOf_add_divOf` 📖	mathematical	—	`AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `modOf` `instMul` `of'` `divOf`	—	`add_comm` `divOf_add_modOf`
`modOf_apply_add_self` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `modOf` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modOf_apply_of_exists_add` `add_comm`
`modOf_apply_of_exists_add` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `modOf`	—	`Finsupp.filter_apply_neg`
`modOf_apply_of_not_exists_add` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `modOf`	—	`Finsupp.filter_apply_pos`
`modOf_apply_self_add` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `modOf` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modOf_apply_of_exists_add`
`mul_of'_divOf` 📖	mathematical	—	`divOf` `AddMonoidAlgebra` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `of'`	—	`ext` `divOf_apply` `of'_apply` `mul_single_apply_aux` `add_comm` `IsCancelAdd.toIsLeftCancelAdd` `mul_one`
`mul_of'_modOf` 📖	mathematical	—	`modOf` `AddMonoidAlgebra` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `of'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring`	—	`ext` `Finsupp.zero_apply` `em` `modOf_apply_self_add` `modOf_apply_of_not_exists_add` `of'_apply` `mul_single_apply_of_not_exists_add` `add_comm`
`of'_divOf` 📖	mathematical	—	`divOf` `of'` `AddMonoidAlgebra` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`divOf.congr_simp` `one_mul` `mul_of'_divOf`
`of'_dvd_iff_modOf_eq_zero` 📖	mathematical	—	`AddMonoidAlgebra` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `nonUnitalSemiring` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `of'` `modOf` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`of'_mul_modOf` `divOf_add_modOf` `add_zero` `dvd_mul_right`
`of'_modOf` 📖	mathematical	—	`modOf` `of'` `AddMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`one_mul` `mul_of'_modOf`
`of'_mul_divOf` 📖	mathematical	—	`divOf` `AddMonoidAlgebra` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `of'`	—	`ext` `divOf_apply` `of'_apply` `single_mul_apply_aux` `IsCancelAdd.toIsLeftCancelAdd` `one_mul`
`of'_mul_modOf` 📖	mathematical	—	`modOf` `AddMonoidAlgebra` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `of'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring`	—	`ext` `Finsupp.zero_apply` `em` `modOf_apply_self_add` `modOf_apply_of_not_exists_add` `of'_apply` `single_mul_apply_of_not_exists_add`
`support_divOf` 📖	mathematical	—	`Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `divOf` `Finset.preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Function.Injective.injOn` `add_right_injective` `IsCancelAdd.toIsLeftCancelAdd` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`zero_divOf` 📖	mathematical	—	`divOf` `AddMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`

---

← Back to Index