Commit 2025-12-01 21:12 b728e145

View on Github →

doc: fix cases of "this <plural noun>" (#32286) Found and fixed with help from Codex.

Estimated changes

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Analysis/InnerProductSpace/Defs.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Analysis/Normed/Group/Constructions.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/End.lean

Modified Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean

Modified Mathlib/Data/ZMod/IntUnitsPower.lean

Modified Mathlib/Topology/Algebra/Monoid.lean