Commit 2021-06-07 07:44 f57f9c8b

feat(ring_theory): define the field/algebra norm (#7636) This PR defines the field norm algebra.norm K L : L →* K, where L is a finite field extension of K. In fact, it defines this for any algebra R S instance, where R and S are integral domains. (With a default value of 1 if S does not have a finite R-basis.) The approach is to basically copy ring_theory/trace.lean and replace trace with det or norm as appropriate.