exponent_pi_eq_zero — Mathlib

English

If at the j-th factor the exponent is zero, then the exponent of the product is zero.

Русский

Если на j-м факторе экспонента равна нулю, то экспонента произведения равна нулю.

LaTeX

$$$\text{If } \operatorname{exponent}(M_j) = 0\text{, then } \operatorname{exponent}\big((i : \iota) \to M i\big) = 0$$$

Lean4

@[to_additive]
theorem exponent_pi_eq_zero {ι : Type*} {M : ι → Type*} [∀ i, Monoid (M i)] {j : ι} (hj : exponent (M j) = 0) :
    exponent ((i : ι) → M i) = 0 := by
  classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push_neg at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j

Похожие утверждения