mathlib3

e2621d93 - chore(number_theory/legendre_symbol/norm_num): remove now unnecessary instance (#16659)

chore(number_theory/legendre_symbol/norm_num): remove now unnecessary instance (#16659) This just removes a shortcut instance in `number_theory/legendre_symnol/norm_num` that was necessary to avoid computability trouble with the meta code, but is no longer so, since the root cause was fixed by #16463.