prod_isUnit_iff — Mathlib

English

In a commutative monoid, IsUnit L.prod is equivalent to saying that every element of L is a unit.

Русский

В коммутативном моноиде IsUnit L.prod эквивалентно тому, что каждый элемент L является единичным.

LaTeX

$$IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m$$

Lean4

@[to_additive]
theorem prod_isUnit_iff {M : Type*} [CommMonoid M] {L : List M} : IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m :=
  by
  refine ⟨fun h => ?_, prod_isUnit⟩
  induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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