mem_lifts_iff — Mathlib

English

An element p ∈ FreeAddMonoid lifts x if and only if the sum of a_i ⨂ m_i over p.toList equals x.

Русский

Элемент p ∈ FreeAddMonoid поднимает x тогда и только тогда сумма a_i ⨂ m_i по p.toList равна x.

LaTeX

$$$$ p \in \text{lifts}(x) \iff \sum_{(a_i, m_i) \in p.toList} a_i \cdot ⨂_i m_i = x $$$$

Lean4

/-- An element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`
if and only if `x` is equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries
`(a, m)` of `p`.
-/
theorem mem_lifts_iff (x : ⨂[R] i, s i) (p : FreeAddMonoid (R × Π i, s i)) :
    p ∈ lifts x ↔ List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p.toList) = x := by
  simp only [lifts, Set.mem_setOf_eq, FreeAddMonoid.toPiTensorProduct]

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