Zulip Chat Archive
Stream: mathlib4
Topic: Complex.int_cast_abs
Yury G. Kudryashov (Feb 01 2024 at 02:17):
IMHO, docs#Complex.int_cast_abs is a bad simp lemma: it "simplifies" by adding complex numbers to the soup.
Yury G. Kudryashov (Feb 01 2024 at 02:23):
:face_palm: I added it in 2020
Last updated: May 02 2025 at 03:31 UTC