FinsetLemmas

Statistics

Metric	Count
Definitions	0
Theorems `associated_lcm_prod`, `lcm_dvd_prod`, `lcm_eq_prod`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_lcm_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Associated` `lcm` `prod` `CommMonoidWithZero.toCommMonoid`	—	`associated_of_dvd_dvd` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `lcm_dvd_prod` `prod_dvd_of_isRelPrime` `instDecompositionMonoidOfNonemptyGCDMonoid` `instNonemptyGCDMonoidOfNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoid` `dvd_lcm`
`lcm_dvd_prod` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `lcm` `prod` `CommMonoidWithZero.toCommMonoid`	—	`lcm_dvd` `dvd_prod_of_mem`
`lcm_eq_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun`	`lcm` `Nat.instCommMonoidWithZero` `instNormalizedGCDMonoidNat` `prod` `Nat.instCommMonoid`	—	`Associated.eq_of_normalized` `Nat.instIsCancelMulZero` `associated_lcm_prod` `Nat.coprime_iff_isRelPrime` `normalize_eq` `Unique.instSubsingleton`

---