def linearIndep {α : Type u_1} {β : Type u_2} [One α] [Mul α] [HPow α ℤ α] [Membership α β] (set : β) : Prop

Equations

• linearIndep set = ∀ x ∈ set, ∀ (xs : List (α × ℤ)), (xs ≠ [] ∧ ∀ y ∈ xs, y.1 ∈ set ∧ y.1 ≠ x) → (List.map (fun (y : α × ℤ) => y.1 ^ y.2) xs).prod ≠ x

@[simp]

theorem Set.linearIndep_empty {α : Type u_1} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] : linearIndep ∅

@[simp]

theorem Set.linearIndep_singleton {α : Type u_1} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] {x : α} : linearIndep {x}

theorem add_eq_iff_eq_sub {α : Type u_2} [AddGroup α] {a b c : α} : a + b = c ↔ a = c - b