Multiset

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

Statistics

Metric	Count
Definitions `gcd`, `lcm`	2
Theorems `dvd_gcd`, `dvd_lcm`, `extract_gcd`, `extract_gcd'`, `gcd_add`, `gcd_cons`, `gcd_dedup`, `gcd_dvd`, `gcd_eq_zero_iff`, `gcd_map_mul`, `gcd_mono`, `gcd_ndinsert`, `gcd_ndunion`, `gcd_ne_zero_iff`, `gcd_singleton`, `gcd_union`, `gcd_zero`, `lcm_add`, `lcm_cons`, `lcm_dedup`, `lcm_dvd`, `lcm_eq_zero_iff`, `lcm_mono`, `lcm_ndinsert`, `lcm_ndunion`, `lcm_ne_zero_iff`, `lcm_singleton`, `lcm_union`, `lcm_zero`, `normalize_gcd`, `normalize_lcm`	31
Total	33

Multiset

Definitions

Name	Category	Theorems
`gcd` 📖	CompOp	16 math math: `gcd_dedup`, `Finset.gcd_def`, `gcd_ndunion`, `extract_gcd`, `gcd_singleton`, `gcd_ndinsert`, `gcd_mono`, `gcd_add`, `dvd_gcd`, `gcd_union`, `gcd_zero`, `gcd_dvd`, `gcd_eq_zero_iff`, `normalize_gcd`, `gcd_map_mul`, `gcd_cons`
`lcm` 📖	CompOp	15 math math: `lcm_eq_zero_iff`, `lcm_add`, `lcm_singleton`, `lcm_mono`, `lcm_dedup`, `lcm_zero`, `Equiv.Perm.lcm_cycleType`, `lcm_cons`, `Finset.lcm_def`, `lcm_union`, `lcm_ndunion`, `normalize_lcm`, `lcm_ndinsert`, `dvd_lcm`, `lcm_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_gcd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`induction_on` `gcd_zero` `instIsEmptyFalse` `gcd_cons`
`dvd_lcm` 📖	mathematical	`Multiset` `instMembership`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd` `dvd_rfl`
`extract_gcd` 📖	mathematical	—	`map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `gcd` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`map_replicate` `eq_replicate` `mul_one` `gcd_eq_zero_iff` `nsmul_singleton` `gcd_dedup` `dedup_nsmul` `LT.lt.ne'` `card_pos` `dedup_singleton` `gcd_singleton` `normalize_one` `map_pmap` `map_id` `pmap_eq_map` `extract_gcd'` `Mathlib.Tactic.Push.not_forall_eq` `gcd_dvd`
`extract_gcd'` 📖	mathematical	`Multiset` `instMembership` `map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `gcd`	`MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`mul_right_eq_self₀` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `normalize_gcd` `gcd_map_mul` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_and_eq` `gcd_eq_zero_iff`
`gcd_add` 📖	mathematical	—	`gcd` `Multiset` `instAdd` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`instCommutativeGcd` `instAssociativeGcd` `fold.congr_simp` `gcd_same` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `fold_add`
`gcd_cons` 📖	mathematical	—	`gcd` `cons` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`fold_cons_left` `instCommutativeGcd` `instAssociativeGcd`
`gcd_dedup` 📖	mathematical	—	`gcd` `dedup`	—	`induction_on` `gcd_zero` `dedup_cons_of_mem` `gcd_cons` `instCommutativeGcd` `instAssociativeGcd` `cons_erase` `fold_cons_left` `gcd_assoc` `gcd_same` `Associated.gcd_eq_left` `associated_normalize` `dedup_cons_of_notMem`
`gcd_dvd` 📖	mathematical	`Multiset` `instMembership`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd` `dvd_rfl`
`gcd_eq_zero_iff` 📖	mathematical	—	`gcd` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`eq_zero_of_zero_dvd` `gcd_dvd` `induction_on` `instIsEmptyFalse` `gcd_zero` `mem_cons_self` `gcd_cons` `mem_cons_of_mem` `gcd_same` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`gcd_map_mul` 📖	mathematical	—	`gcd` `map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`induction_on` `gcd_zero` `MulZeroClass.mul_zero` `map_cons` `gcd_cons` `Associated.gcd_eq_right` `Associated.mul_right` `normalize_associated`
`gcd_mono` 📖	mathematical	`Multiset` `instHasSubset`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `gcd`	—	`dvd_gcd` `gcd_dvd`
`gcd_ndinsert` 📖	mathematical	—	`gcd` `ndinsert` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`gcd_dedup` `dedup_ext` `gcd_cons`
`gcd_ndunion` 📖	mathematical	—	`gcd` `ndunion` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`gcd_dedup` `dedup_ext` `gcd_add`
`gcd_ne_zero_iff` 📖	mathematical	—	`Multiset` `instMembership`	—	—
`gcd_singleton` 📖	mathematical	—	`gcd` `Multiset` `instSingleton` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`instCommutativeGcd` `instAssociativeGcd` `fold_singleton` `gcd_zero_right`
`gcd_union` 📖	mathematical	—	`gcd` `Multiset` `instUnion` `GCDMonoid.gcd` `NormalizedGCDMonoid.toGCDMonoid`	—	`gcd_dedup` `dedup_ext` `gcd_add`
`gcd_zero` 📖	mathematical	—	`gcd` `Multiset` `instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`fold_zero` `instCommutativeGcd` `instAssociativeGcd`
`lcm_add` 📖	mathematical	—	`lcm` `Multiset` `instAdd` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`instCommutativeLcm` `instAssociativeLcm` `fold.congr_simp` `lcm_same` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `fold_add`
`lcm_cons` 📖	mathematical	—	`lcm` `cons` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`fold_cons_left` `instCommutativeLcm` `instAssociativeLcm`
`lcm_dedup` 📖	mathematical	—	`lcm` `dedup`	—	`induction_on` `lcm_zero` `dedup_cons_of_mem` `lcm_cons` `instCommutativeLcm` `instAssociativeLcm` `cons_erase` `fold_cons_left` `lcm_assoc` `lcm_same` `lcm_eq_of_associated_left` `associated_normalize` `dedup_cons_of_notMem`
`lcm_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`induction_on` `lcm_zero` `instIsEmptyFalse` `lcm_cons`
`lcm_eq_zero_iff` 📖	mathematical	—	`lcm` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `instMembership`	—	`induction_on` `lcm_zero` `NeZero.one` `lcm_cons`
`lcm_mono` 📖	mathematical	`Multiset` `instHasSubset`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm`	—	`lcm_dvd` `dvd_lcm`
`lcm_ndinsert` 📖	mathematical	—	`lcm` `ndinsert` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`lcm_dedup` `dedup_ext` `lcm_cons`
`lcm_ndunion` 📖	mathematical	—	`lcm` `ndunion` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`lcm_dedup` `dedup_ext` `lcm_add`
`lcm_ne_zero_iff` 📖	mathematical	—	`Multiset` `instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`lcm_eq_zero_iff`
`lcm_singleton` 📖	mathematical	—	`lcm` `Multiset` `instSingleton` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`instCommutativeLcm` `instAssociativeLcm` `fold_singleton` `lcm_one_right`
`lcm_union` 📖	mathematical	—	`lcm` `Multiset` `instUnion` `GCDMonoid.lcm` `NormalizedGCDMonoid.toGCDMonoid`	—	`lcm_dedup` `dedup_ext` `lcm_add`
`lcm_zero` 📖	mathematical	—	`lcm` `Multiset` `instZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`fold_zero` `instCommutativeLcm` `instAssociativeLcm`
`normalize_gcd` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid` `gcd`	—	`induction_on` `gcd_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `gcd_cons` `normalize_gcd`
`normalize_lcm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid` `lcm`	—	`induction_on` `lcm_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `lcm_cons` `normalize_lcm`

---

← Back to Index