Finset

📁 Source: Mathlib/Algebra/GCDMonoid/Finset.lean

Statistics

Metric	Count
Definitions `gcd`, `lcm`	2
Theorems `finsetGcd_nonneg`, `dvd_gcd`, `dvd_gcd_iff`, `dvd_lcm`, `extract_gcd`, `extract_gcd'`, `gcd_congr`, `gcd_cons`, `gcd_def`, `gcd_div_eq_one`, `gcd_div_id_eq_one`, `gcd_dvd`, `gcd_empty`, `gcd_eq_gcd_filter_ne_zero`, `gcd_eq_gcd_image`, `gcd_eq_of_dvd_sub`, `gcd_eq_zero_iff`, `gcd_image`, `gcd_insert`, `gcd_mono`, `gcd_mono_fun`, `gcd_mul_left`, `gcd_mul_right`, `gcd_ne_zero_iff`, `gcd_singleton`, `gcd_union`, `lcm_congr`, `lcm_def`, `lcm_dvd`, `lcm_dvd_iff`, `lcm_empty`, `lcm_eq_lcm_image`, `lcm_eq_zero_iff`, `lcm_image`, `lcm_insert`, `lcm_mono`, `lcm_mono_fun`, `lcm_ne_zero_iff`, `lcm_singleton`, `lcm_union`, `normalize_gcd`, `normalize_lcm`	42
Total	44

Finset

Definitions

Name	Category	Theorems
`gcd` 📖	CompOp	27 math math: `gcd_empty`, `gcd_dvd`, `Polynomial.content_eq_gcd_range_of_lt`, `dvd_gcd`, `gcd_eq_zero_iff`, `extract_gcd`, `Int.finsetGcd_nonneg`, `gcd_image`, `gcd_cons`, `gcd_def`, `gcd_congr`, `gcd_mul_left`, `gcd_eq_gcd_filter_ne_zero`, `gcd_mono`, `dvd_gcd_iff`, `extract_gcd'`, `gcd_union`, `gcd_singleton`, `gcd_insert`, `gcd_eq_of_dvd_sub`, `gcd_div_id_eq_one`, `gcd_mul_right`, `gcd_eq_gcd_image`, `Polynomial.content_eq_gcd_range_succ`, `normalize_gcd`, `gcd_mono_fun`, `gcd_div_eq_one`
`lcm` 📖	CompOp	30 math math: `Pi.addOrderOf`, `Monoid.exponent_pi`, `lcm_singleton`, `lcm_dvd_prod`, `normalize_lcm`, `associated_lcm_prod`, `AddMonoid.exponent_pi`, `Function.minimalPeriod_piMap_fintype`, `Monoid.lcm_orderOf_eq_exponent`, `Monoid.lcm_orderOf_dvd_exponent`, `lcm_empty`, `lcm_def`, `lcm_eq_prod`, `Pi.orderOf`, `lcm_dvd`, `ArithmeticFunction.carmichael_finset_lcm`, `lcm_eq_lcm_image`, `lcm_image`, `ArithmeticFunction.carmichael_finset_prod`, `AddMonoid.lcm_addOrderOf_eq_exponent`, `lcm_mono_fun`, `lcm_union`, `ArithmeticFunction.carmichael_factorization`, `lcm_insert`, `lcm_dvd_iff`, `AddMonoid.lcm_addOrderOf_dvd_exponent`, `lcm_eq_zero_iff`, `lcm_mono`, `dvd_lcm`, `lcm_congr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_gcd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd_iff`
`dvd_gcd_iff` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`Multiset.dvd_gcd`
`dvd_lcm` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd_iff` `dvd_rfl`
`extract_gcd` 📖	mathematical	`Nonempty`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `gcd` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`gcd_eq_zero_iff` `mul_one` `gcd_eq_gcd_image` `image_const` `gcd_singleton` `normalize_one` `extract_gcd'` `Mathlib.Tactic.Push.not_forall_eq` `gcd_dvd`
`extract_gcd'` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `gcd`	`gcd` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`mul_right_eq_self₀` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `normalize_gcd` `gcd_mul_left` `gcd_congr` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_and_eq` `gcd_eq_zero_iff`
`gcd_congr` 📖	mathematical	—	`gcd`	—	`fold_congr` `instCommutativeGcd` `instAssociativeGcd`
`gcd_cons` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`gcd` `cons` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`fold_cons` `instCommutativeGcd` `instAssociativeGcd`
`gcd_def` 📖	mathematical	—	`gcd` `Multiset.gcd` `Multiset.map` `val`	—	—
`gcd_div_eq_one` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`gcd` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`extract_gcd` `gcd_congr` `mul_div_cancel_left₀` `gcd_eq_zero_iff`
`gcd_div_id_eq_one` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`gcd` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`gcd_div_eq_one`
`gcd_dvd` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd_iff` `dvd_rfl`
`gcd_empty` 📖	mathematical	—	`gcd` `Finset` `instEmptyCollection` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	—
`gcd_eq_gcd_filter_ne_zero` 📖	mathematical	—	`gcd` `filter` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`filter_union_filter_not_eq` `gcd_union` `induction_on` `filter_empty` `filter_insert` `gcd_insert` `gcd_same` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `gcd_zero_left` `normalize_gcd`
`gcd_eq_gcd_image` 📖	mathematical	—	`gcd` `image`	—	`gcd_image`
`gcd_eq_of_dvd_sub` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NormalizedGCDMonoid.toGCDMonoid` `gcd`	—	`induction_on` `instIsEmptyFalse` `gcd_zero_right` `gcd_insert` `gcd_comm` `gcd_assoc` `mem_insert_of_mem` `gcd_eq_of_dvd_sub_right` `mem_insert_self`
`gcd_eq_zero_iff` 📖	mathematical	—	`gcd` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`cons_induction_on` `instIsEmptyFalse`
`gcd_image` 📖	mathematical	—	`gcd` `image`	—	`induction` `image_insert` `gcd_insert`
`gcd_insert` 📖	mathematical	—	`gcd` `Finset` `instInsert` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`insert_eq_of_mem` `gcd_eq_right_iff` `Multiset.normalize_gcd` `gcd_dvd` `fold_insert` `instCommutativeGcd` `instAssociativeGcd`
`gcd_mono` 📖	mathematical	`Finset` `instHasSubset`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd` `gcd_dvd`
`gcd_mono_fun` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd` `Dvd.dvd.trans` `gcd_dvd`
`gcd_mul_left` 📖	mathematical	—	`gcd` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`induction_on` `MulZeroClass.mul_zero` `gcd_insert` `gcd_mul_left` `Associated.gcd_eq_right` `Associated.mul_right` `normalize_associated`
`gcd_mul_right` 📖	mathematical	—	`gcd` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`induction_on` `MulZeroClass.zero_mul` `gcd_insert` `gcd_mul_right` `Associated.gcd_eq_right` `Associated.mul_left` `normalize_associated`
`gcd_ne_zero_iff` 📖	mathematical	—	`Finset` `SetLike.instMembership` `instSetLike`	—	—
`gcd_singleton` 📖	mathematical	—	`gcd` `Finset` `instSingleton` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`Multiset.gcd_singleton`
`gcd_union` 📖	mathematical	—	`gcd` `Finset` `instUnion` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`induction_on` `empty_union` `gcd_empty` `gcd_zero_left` `normalize_gcd` `insert_union` `gcd_insert` `gcd_assoc`
`lcm_congr` 📖	mathematical	—	`lcm`	—	`fold_congr` `instCommutativeLcm` `instAssociativeLcm`
`lcm_def` 📖	mathematical	—	`lcm` `Multiset.lcm` `Multiset.map` `val`	—	—
`lcm_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd_iff`
`lcm_dvd_iff` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`Multiset.lcm_dvd`
`lcm_empty` 📖	mathematical	—	`lcm` `Finset` `instEmptyCollection` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	—
`lcm_eq_lcm_image` 📖	mathematical	—	`lcm` `image`	—	`lcm_image`
`lcm_eq_zero_iff` 📖	mathematical	—	`lcm` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finset` `SetLike.instMembership` `instSetLike`	—	—
`lcm_image` 📖	mathematical	—	`lcm` `image`	—	`induction` `image_insert` `lcm_insert`
`lcm_insert` 📖	mathematical	—	`lcm` `Finset` `instInsert` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`insert_eq_of_mem` `lcm_eq_right_iff` `Multiset.normalize_lcm` `dvd_lcm` `fold_insert` `instCommutativeLcm` `instAssociativeLcm`
`lcm_mono` 📖	mathematical	`Finset` `instHasSubset`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd` `dvd_lcm`
`lcm_mono_fun` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd` `Dvd.dvd.trans` `dvd_lcm`
`lcm_ne_zero_iff` 📖	—	—	—	—	—
`lcm_singleton` 📖	mathematical	—	`lcm` `Finset` `instSingleton` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`Multiset.lcm_singleton`
`lcm_union` 📖	mathematical	—	`lcm` `Finset` `instUnion` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`induction_on` `empty_union` `lcm_empty` `lcm_one_left` `normalize_lcm` `insert_union` `lcm_insert` `lcm_assoc`
`normalize_gcd` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid` `gcd`	—	`Multiset.normalize_gcd`
`normalize_lcm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid` `lcm`	—	`Multiset.normalize_lcm`

Finset.Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsetGcd_nonneg` 📖	mathematical	—	`Finset.gcd` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `Int.instNormalizedGCDMonoid`	—	`Finset.cons_induction_on` `instReflLe` `Finset.gcd_cons` `Int.coe_gcd`

---

← Back to Index