Commit 2024-02-14 23:28 6fc84347

View on Github →

chore: Turn Complex.int_cast_abs around (#10543) A goal about real numbers should not suddenly turn into a goal about complex numbers!

Estimated changes

modified theorem Complex.norm_int
added theorem Complex.abs_intCast
modified theorem Complex.int_cast_abs