[Merged by Bors] - feat: compute Monoid.exponent as the lcm over pi types and Prod

[j-loreaux]

---

[eric-wieser]

Is this true as an Iff with an existential?

[eric-wieser]

(and is the Prod version too, with an or?)

[j-loreaux]

Note: the version I provided here does not assume Fintype ι as Monoid.exponent_pi does. Without that, the ↔ does not hold (consider the product Π n, ZMod n for instance).

With the Fintype ι condition, then yes, it's true, but it follows immediately from Finset.lcm_eq_zero_iff, and I would expect users to use that if they want this result. Similarly, the prod version holds, but follows immediately from lcm_eq_zero_iff (once I switch from Nat.lcm to lcm, which I just realized I should have done).

So, these are the lemmas, but I propose not including them:

@[to_additive]
lemma Monoid.exponent_pi_zero_iff {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, Monoid (M i)] :
    exponent ((i : ι) → M i) = 0 ↔ ∃ i, exponent (M i) = 0 := by
  rw [Monoid.exponent_pi, Finset.lcm_eq_zero_iff]
  simp

@[to_additive]
theorem Monoid.exponent_prod_zero_iff {M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] :
    exponent (M₁ × M₂) = 0 ↔ (exponent M₁ = 0) ∨ (exponent M₂ = 0) := by
  rw [exponent_prod, lcm_eq_zero_iff]

[eric-wieser]

bors d+

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style