Norm groups under algebra isomorphisms

An isomorphism of extensions preserves the norm subgroup of the ground field's units. This permits norm-index calculations in a model extension to be used for any isomorphic extension. The proof uses Mathlib's Algebra.norm_eq_of_algEquiv. The identity extension has the full norm group, as does every finite extension of an algebraically closed field, since its algebra map is an isomorphism.

@[simp]

theorem TauCeti.normGroup_self (K : Type u_1) [Field K] : normGroup K K = ⊤

The identity extension has the whole unit group as its norm group.

theorem AlgEquiv.normGroup_eq {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Module.Finite K L] [Module.Finite K M] (e : L ≃ₐ[K] M) : TauCeti.normGroup K L = TauCeti.normGroup K M

Isomorphic finite field extensions have the same norm group in the ground field.

@[simp]

theorem TauCeti.normGroup_eq_top_of_isAlgClosed (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [FiniteDimensional K L] : normGroup K L = ⊤

Every unit is a norm in a finite extension of an algebraically closed field.