feat(Algebra/Group/Even): "Advanced" lemmas about even elements. (#20272

)

Add construction of subgroup of even elements / squares.
Add result that squares (`IsSquare`) are non-negative.

These results cannot be added to `Mathlib.Algebra.Group.Even` directly because of import restrictions.
This PR is split off from #16094

Mathlib.lean

@@ -319,6 +319,7 @@ import Mathlib.Algebra.Group.Semiconj.Units
 import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
+import Mathlib.Algebra.Group.Subgroup.Even
 import Mathlib.Algebra.Group.Subgroup.Finite
 import Mathlib.Algebra.Group.Subgroup.Finsupp
 import Mathlib.Algebra.Group.Subgroup.Ker

Mathlib/Algebra/Group/Subgroup/Even.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2024 Artie Khovanov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Artie Khovanov
+-/
+import Mathlib.Algebra.Group.Even
+import Mathlib.Algebra.Group.Subgroup.Defs
+
+/-!
+# Squares and even elements
+
+This file defines the subgroup of squares / even elements in an abelian group.
+-/
+
+namespace Subsemigroup
+variable {S : Type*} [CommSemigroup S] {a : S}
+
+variable (S) in
+/--
+In a commutative semigroup `S`, `Subsemigroup.squareIn S` is the subsemigroup of squares in `S`.
+-/
+@[to_additive
+"In a commutative additive semigroup `S`, the type `AddSubsemigroup.evenIn S`
+is the subsemigroup of even elements of `S`."]
+def squareIn : Subsemigroup S where
+  carrier := {s : S | IsSquare s}
+  mul_mem' := IsSquare.mul
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn S ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn S = {s : S | IsSquare s} := rfl
+
+end Subsemigroup
+
+namespace Submonoid
+variable {M : Type*} [CommMonoid M] {a : M}
+
+variable (M) in
+/--
+In a commutative monoid `M`, `Submonoid.squareIn M` is the submonoid of squares in `M`.
+-/
+@[to_additive
+"In a commutative additive monoid `M`, the type `AddSubmonoid.evenIn M`
+is the submonoid of even elements of `M`."]
+def squareIn : Submonoid M where
+  __ := Subsemigroup.squareIn M
+  one_mem' := IsSquare.one
+
+@[to_additive (attr := simp)]
+theorem squareIn_toSubsemigroup : (squareIn M).toSubsemigroup = .squareIn M := rfl
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn M ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn M = {s : M | IsSquare s} := rfl
+
+end Submonoid
+
+namespace Subgroup
+variable {G : Type*} [CommGroup G] {a : G}
+
+variable (G) in
+/--
+In an abelian group `G`, `Subgroup.squareIn G` is the subgroup of squares in `G`.
+-/
+@[to_additive
+"In an abelian additive group `G`, the type `AddSubgroup.evenIn G` is
+the subgroup of even elements in `G`."]
+def squareIn : Subgroup G where
+  __ := Submonoid.squareIn G
+  inv_mem' := IsSquare.inv
+
+@[to_additive (attr := simp)]
+theorem squareIn_toSubmonoid : (squareIn G).toSubmonoid = .squareIn G := rfl
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn G ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn G = {s : G | IsSquare s} := rfl
+
+end Subgroup

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -20,6 +20,12 @@ open Function Int
 
 variable {α M R : Type*}
 
+theorem IsSquare.nonneg [Semiring R] [LinearOrder R] [IsRightCancelAdd R]
+    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R]
+    {x : R} (h : IsSquare x) : 0 ≤ x := by
+  rcases h with ⟨y, rfl⟩
+  exact mul_self_nonneg y
+
 namespace MonoidHom
 
 variable [Ring R] [Monoid M] [LinearOrder M] [MulLeftMono M] (f : R →* M)

Mathlib/Tactic/ToAdditive/Frontend.lean

@@ -1027,6 +1027,7 @@ def fixAbbreviation : List String → List String
   | "add" :: "_" :: "indicator" :: s  => "indicator" :: fixAbbreviation s
   | "is" :: "Square" :: s             => "even" :: fixAbbreviation s
   | "Is" :: "Square" :: s             => "Even" :: fixAbbreviation s
+  | "square" :: "In" :: s             => "evenIn" :: fixAbbreviation s
   -- "Regular" is well-used in mathlib with various meanings (e.g. in
   -- measure theory) and a direct translation
   -- "regular" --> ["add", "Regular"] in `nameDict` above seems error-prone.