mem_mulSpan — Mathlib

English

An element a belongs to mulSpan(s) exactly when there exists a function ε: ambient → ℤ with values in {−1,0,1} on s such that a = ∏_{b∈s} b^{ε(b)}.

Русский

Элемент a принадлежит mulSpan(s) тогда и только тогда, когда существует функция ε: окружение → ℤ, принимающая на s значения −1,0,1, такая что a = ∏_{b∈s} b^{ε(b)}.

LaTeX

$$$a \in mulSpan(s) \iff \exists \varepsilon: \alpha \to \mathbb{Z}, \; (\forall b, \varepsilon(b) \in \{-1,0,1\}) \land \prod_{b\in s} b^{\varepsilon(b)} = a$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_mulSpan : a ∈ mulSpan s ↔ ∃ ε : α → ℤ, (∀ a, ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a := by
  simp [mulSpan]

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