Theorem: neg_in_𝔻 (RMT4/defs.lean)

State before:
u : ℂ
U V W : Set ℂ
⊢ u ∈ 𝔻 → -u ∈ 𝔻
Tactic:
simp [𝔻]
State after:
no goals