Commit 2024-05-15 09:43 3e51ad14

move(Algebra/Parity): Split file (#12829) Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, Algebra.Parity currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles. This PR moves the content of Algebra.Parity to

• Algebra.Group.Even for the definition of IsSquare and Even
• Algebra.Ring.Parity for the definition of Odd and ring properties of Even
• Algebra.Order.Group.Abs, Algebra.Order.Ring.Abs, Algebra.Order.Ring.Canonical, Algebra.Order.Sub.Canonical, Algebra.GroupPower.Order for the various algebraic order properties of Even and Odd As a result, Even/Odd are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in Algebra.Ring.Parity are stated using Set.range, hence I had to weaken a few assert_not_exists to forbidding Data.Set.Basic instead of Data.Set.Defs. This is inconsequential. A side-effect of this PR is that I had to move some bit0/bit1 lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in Algebra.Parity. As a result, I had to reprove a few lemmas in Algebra.GroupPower.Order. I took the opportunity to generalise them. This is a followup to https://github.com/leanprover-community/mathlib/pull/17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.