α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i in range n, x ^ i = 0
⊢ x = -1 ∧ Even n
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i = 0 ↔ x = -1 ∧ Even n
refine' ⟨fun h => _, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i in range n, x ^ i ≠ 0
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i in range n, x ^ i = 0
⊢ x = -1 ∧ Even n
contrapose! h
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i in range n, x ^ i ≠ 0
have hx := eq_or_ne x (-1)
case inl
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i in range n, x ^ i ≠ 0

case inr
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
cases' hx with hx hx
no goals
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i in range n, x ^ i = 0
simp only [h, hn, neg_one_geom_sum, if_true]
case inl
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
case inl
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i in range n, x ^ i ≠ 0
rw [hx, neg_one_geom_sum]
no goals
case inl
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
simp only [h hx, ne_eq, ite_eq_left_iff, one_ne_zero, not_forall, exists_prop, and_true]
no goals
case inr
α : Type u
β : Type ?u.252702
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
exact geom_sum_ne_zero hx hn