Commit 2025-05-29 18:27 520939fa
View on Github →feat(Analysis/RCLike): add theorem RCLike.zero_im and fix name of RCLike.zero_re (#25077)
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RCLike.2Ezero_re'/with/519422684