a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 (n + 1))
a : ℕ
a1 : 1 < a
n : ℕ
⊢ IsPell (pellZd a1 (n + 1))
let o := isPell_one a1
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 n * { re := ↑a, im := 1 })
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 (n + 1))
simp
no goals
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 n * { re := ↑a, im := 1 })
exact Pell.isPell_mul (isPell_pellZd n) o