Norm groups of finite real extensions

Every finite extension of ℝ is isomorphic to ℝ or ℂ, by Mathlib's Real.nonempty_algEquiv_or. Its norm group is therefore all real units in degree one, and the positive units in degree two. In both cases its norm index equals its degree. The degree-two computation uses TauCeti.normGroup_real_complex and Mathlib's Units.index_posSubgroup.

theorem TauCeti.normGroup_real_eq (L : Type u_1) [Field L] [Algebra ℝ L] [FiniteDimensional ℝ L] : normGroup ℝ L = if Module.finrank ℝ L = 1 then ⊤ else Units.posSubgroup ℝ

The norm group of a finite real extension is all real units in degree one and the positive real units in degree two.

@[simp]

theorem TauCeti.index_normGroup_real (L : Type u_1) [Field L] [Algebra ℝ L] [FiniteDimensional ℝ L] : (normGroup ℝ L).index = Module.finrank ℝ L

The norm index of every finite extension of the reals equals its degree.