Commit 2025-03-08 08:24 1a7567c3

View on Github →

chore: create the Algebra.Notation folder (#22640) Currently, basic algebraic notation is scattered across several files. Move those files together into a new Algebra.Notation folder. Explain its purpose by adding two README.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Expr.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/Hom/Defs.lean

Modified Mathlib/Algebra/Group/Pi/Basic.lean

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Group/Support.lean

Modified Mathlib/Algebra/NeZero.lean

Renamed Mathlib/Algebra/Group/Operations.lean to Mathlib/Algebra/Notation/Defs.lean

added theorem Subsingleton.eq_one

Renamed Mathlib/Algebra/ZeroOne/Lemmas.lean to Mathlib/Algebra/Notation/Lemmas.lean

Renamed Mathlib/Algebra/Group/Pi/Notation.lean to Mathlib/Algebra/Notation/Pi.lean

Renamed Mathlib/Algebra/ZeroOne/Prod.lean to Mathlib/Algebra/Notation/Prod.lean

Created Mathlib/Algebra/Notation/README.md

Modified Mathlib/Algebra/Order/Field/Pi.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/Order/Sum.lean

Modified Mathlib/Algebra/Order/ZeroLEOne.lean

Created Mathlib/Algebra/README.md

Modified Mathlib/Data/Nat/Pairing.lean

Modified Mathlib/Data/Num/Basic.lean

Deleted Mathlib/Data/One/Defs.lean

deleted theorem Subsingleton.eq_one

Modified Mathlib/Data/PNat/Defs.lean

Modified Mathlib/Data/Part.lean

Modified Mathlib/Data/Set/Insert.lean

Modified Mathlib/Lean/Meta/RefinedDiscrTree/Pi.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified MathlibTest/byContra.lean

Modified scripts/noshake.json