isUnit_iff — Mathlib

English

For a family of monoids M_i, an element x ∈ ∏_i M_i is a unit if and only if every coordinate x_i is a unit in M_i.

Русский

Для семейства моноидов M_i элемент x = (x_i) в произведении ∏_i M_i является единицей тогда и только тогда, когда каждая координата x_i является единицей в M_i.

LaTeX

$$IsUnit x iff ∀ i, IsUnit (x i)$$

Lean4

@[to_additive]
theorem isUnit_iff : IsUnit x ↔ ∀ i, IsUnit (x i) :=
  by
  simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]
  exact Classical.skolem (p := fun i y ↦ x i * y = 1 ∧ y * x i = 1).symm

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