A square times an even power of a unit

A candidate for Mathlib.Algebra.Group.Even, next to IsSquare.mul and IsSquare.div: in a commutative monoid, y ^ 2 = v u ^ D with u a unit and D even makes v a square, as for the value v = f(a / b) of a polynomial when y ^ 2 = f(a / b) b ^ D is the value of a binary form of even degree D at (a, b). The file imports Mathlib.Algebra.Group.Units.Defs as well, since Mathlib.Algebra.Group.Even does not know units.

Main statements

• IsUnit.isSquare_of_sq_eq_mul_pow: y ^ 2 = v u ^ D with u a unit and D even makes v a square.

theorem IsUnit.isSquare_of_sq_eq_mul_pow {M : Type u_1} [CommMonoid M] {y v u : M} (hu : IsUnit u) {D : ℕ} (hD : Even D) (h : y ^ 2 = v * u ^ D) : IsSquare v

y ^ 2 = v u ^ D with u a unit and D even makes v a square: v = (y u⁻¹ ^ (D / 2)) ^ 2. Mathlib has IsSquare.mul and, in a group, IsSquare.div.