Theorem: IMOSL.IMO2017A6.good_map_add_one_eq_zero_iff (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) = 0 ↔ x = 0
Tactic:
rw [good_map_eq_zero_iff h h0, add_left_eq_self]
State after:
no goals