Squares of units

This file relates squares in a monoid to squares in its group of units.

Main results

• TauCeti.isSquare_units_val_iff: a unit is a square exactly when its underlying monoid element is a square.

@[simp]

theorem TauCeti.isSquare_units_val_iff {M : Type u_1} [Monoid M] {u : Mˣ} : IsSquare ↑u ↔ IsSquare u

A unit is a square exactly when its underlying monoid element is a square.