mulLECancellable_prod — Mathlib

English

In a commutative monoid, the product ∏_{i∈s} f(i) is MulLECancellable if and only if each f(i) is MulLECancellable on its own.

Русский

Произведение ∏_{i∈s} f(i) имеет свойство MulLECancellable тогда и только тогда, когда каждый f(i) имеет это свойство отдельно.

LaTeX

$$$ \\forall s : \\mathrm{Finset} \\iota, f : \\iota \\to \\alpha \\, [\\text{CommMonoid } \\alpha], [\\text{LE } \\alpha], [\\text{MulLeftMono } \\alpha], ( MulLECancellable (\\prod_{i\\in s} f i) \\leftrightarrow \\forall i \\in s, MulLECancellable (f i) ). $$$

Lean4

@[to_additive (attr := simp)]
theorem mulLECancellable_prod : MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i⦄, i ∈ s → MulLECancellable (f i) := by
  induction s using Finset.cons_induction <;> simp [*]

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