Commit 2026-05-25 10:31 773df06e

View on Github →

feat: missing nnratCast lemmas for RCLike (#39620)

Estimated changes

added theorem RCLike.nnratCast_im
added theorem RCLike.nnratCast_re
modified theorem RCLike.ofReal_nnratCast