spanFinset_ne_zero

Mathlib.RingTheory.FractionalIdeal.Operations

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.spanFinset_ne_zero

English

spanFinset R s f ≠ 0 if and only if there exists j ∈ s with f(j) ≠ 0.

Русский

spanFinset R s f ≠ 0 тогда существует j ∈ s с f(j) ≠ 0.

LaTeX

$$$ \operatorname{spanFinset} R\, s\, f \neq 0 \iff \exists j \in s,\; f(j) \neq 0 $$$

Lean4

theorem spanFinset_ne_zero {ι : Type*} {s : Finset ι} {f : ι → K} : spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0 := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru