Square classes of real numbers

A nonzero real number is a square exactly when it is positive, so the square-class group of ℝ has two elements: the trivial class and the class of -1. This file records that description in the form used to read signs off square-class invariants such as the discriminant of a quadratic form.

Main results

• Units.isSquare_iff_pos: a real unit is a square iff it is positive.
• Units.squareClass_eq_zero_iff_pos: a real unit has trivial square class iff it is positive.
• Units.squareClass_eq_squareClass_neg_one_iff_neg: a real unit has the square class of -1 iff it is negative.
• TauCeti.sum_squareClass_eq_ncard_nsmul: the square classes of a finite family of real units add up to the number of negative members times the class of -1.
• TauCeti.nsmul_squareClass_neg_one_eq_zero_iff_even: n • [-1] vanishes in the real square-class group exactly when n is even.
• TauCeti.eq_one_or_eq_squareClassHom_neg_one: every real square class is either the trivial class or the class of -1, in multiplicative notation.
• TauCeti.natCard_units_quotient_square_real: the multiplicative real square-class group has two elements.

@[simp]

theorem Units.isSquare_iff_pos (u : ℝˣ) : IsSquare u ↔ 0 < ↑u

A real unit is a square exactly when it is positive.

theorem Units.square_eq_posSubgroup_real : Subgroup.square ℝˣ = posSubgroup ℝ

The squares in the real unit group are exactly the positive units.

theorem Units.squareClass_eq_zero_iff_pos (u : ℝˣ) : TauCeti.squareClass u = 0 ↔ 0 < ↑u

A real unit has trivial square class exactly when it is positive.

This is not tagged @[simp] because squareClass_eq_zero_iff rewrites its left-hand side first; Units.isSquare_iff_pos supplies the resulting simp-normal rule.

@[simp]

theorem Units.squareClass_eq_squareClass_neg_one_iff_neg (u : ℝˣ) : TauCeti.squareClass u = TauCeti.squareClass (-1) ↔ ↑u < 0

A real unit has the square class of -1 exactly when it is negative.

@[simp]

theorem TauCeti.nsmul_squareClass_neg_one_eq_zero_iff_even (n : ℕ) : n • squareClass (-1) = 0 ↔ Even n

The n-th multiple of the square class of -1 in the real square-class group vanishes exactly when n is even.

theorem TauCeti.sum_squareClass_eq_ncard_nsmul {ι : Type u_1} [Fintype ι] (w : ι → ℝˣ) : ∑ i : ι, squareClass (w i) = {i : ι | ↑(w i) < 0}.ncard • squareClass (-1)

The square classes of a finite family of real units add up to the number of negative members times the class of -1.

theorem TauCeti.eq_one_or_eq_squareClassHom_neg_one (x : ℝˣ ⧸ Subgroup.square ℝˣ) : x = 1 ∨ x = squareClassHom (-1)

Every real multiplicative square class is either trivial or the class of -1.

theorem TauCeti.natCard_units_quotient_square_real : Nat.card (ℝˣ ⧸ Subgroup.square ℝˣ) = 2

The multiplicative real square-class group has exactly two elements, the trivial class and the class of -1.