Theorem: multibrot_zero (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ∈ multibrot d
Tactic:
apply multibrot_of_zero
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (f d 0)^[?n] ↑0 = 0

case n
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ℕ

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (f d 0)^[?n] ↑0 = 0

case n
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ℕ
Tactic:
rw [Function.iterate_zero_apply, coe_zero]
State after:
no goals