Commit 2025-01-03 07:21 b2158cc4

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/Subgroup/Even.lean

added theorem Subgroup.coe_squareIn

added theorem Subgroup.mem_squareIn

added def Subgroup.squareIn

added theorem Subgroup.squareIn_toSubmonoid

added theorem Submonoid.coe_squareIn

added theorem Submonoid.mem_squareIn

added def Submonoid.squareIn

added theorem Submonoid.squareIn_toSubsemigroup

added theorem Subsemigroup.coe_squareIn

added theorem Subsemigroup.mem_squareIn

added def Subsemigroup.squareIn

Modified Mathlib/Algebra/Order/Ring/Basic.lean

added theorem IsSquare.nonneg

Modified Mathlib/Tactic/ToAdditive/Frontend.lean