Commit 2025-02-06 16:52 1c4196c6

View on Github →

chore(Data/Complex/Abs): add protected to results that already exists in root namespace (#21454) The names of several results about Complex.abs collide with results in the root namespace when the namespace Complex is opened. To avoid this inconvenience, this PR protects the name of these results.

Estimated changes

modified theorem Complex.norm_nnratCast
deleted theorem Complex.abs_abs
modified theorem Complex.abs_add_mul_I
modified theorem Complex.abs_im_eq_abs
modified theorem Complex.abs_intCast
deleted theorem Complex.abs_pow
modified theorem Complex.abs_re_eq_abs
deleted theorem Complex.abs_two
deleted theorem Complex.sq_abs