How do I put jQuery code in an external file in WordPress theme?

I am relatively new to Javascript/jQuery so please bear with me.

I’m designing a custom WordPress theme and I have been using jQuery to make some changes to the main navigation menu that is generated in my header file (header.php). I have been adding code like this inside the head tag:

<script src="//ajax.googleapis.com/ajax/libs/jquery/1.9.1/jquery.min.js" ></script>
<script>
  $(document).ready(function(){
    $('nav').mouseover(function() {
      // my mousecode here...
    }); // end mouseover
  }); // end ready
</script>

My question is simple really. My scripts have gotten so long that I want to move them to their own file (perhaps nav-mouse-events.js) and call them from within header.php. How do I do this? Is it as simple as putting the code inbetween the second script tags into a file named nav-mouse-events.js and then adding this to the head tag?

<script src="nav-mouse-events.js"></script>

Or do I need to do something more complicated? Do I need to call jQuery from the new external file or header.php?