case intro.intro.intro
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
V₂ : Type v'
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < card t
f : W → L
sum : ∑ e in t, f e • e = 0
total : ∑ e in t, f e = 0
nonzero : ∃ x, x ∈ t ∧ f x ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ 0 < f x
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
V₂ : Type v'
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < card t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ 0 < f x
obtain ⟨f, sum, total, nonzero⟩ := exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card h
no goals
case intro.intro.intro
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
V₂ : Type v'
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < card t
f : W → L
sum : ∑ e in t, f e • e = 0
total : ∑ e in t, f e = 0
nonzero : ∃ x, x ∈ t ∧ f x ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ 0 < f x
exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩