Commit 2025-12-01 21:50 2ddd611e

View on Github →

doc: fix a/an articles (4/4) (#32293) Found and fixed by a script (due to Codex). Then manually reviewed.

Estimated changes

Modified Mathlib/Tactic/CC/Addition.lean

Modified Mathlib/Tactic/DeriveEncodable.lean

Modified Mathlib/Tactic/FieldSimp.lean

Modified Mathlib/Tactic/GCongr/Core.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/TermCongr.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Group/Quotient.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

Modified Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Convenient/GeneratedBy.lean

Modified Mathlib/Topology/Homotopy/Equiv.lean

Modified Mathlib/Topology/Maps/Proper/Basic.lean

Modified Mathlib/Topology/Maps/Proper/UniversallyClosed.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

Modified Mathlib/Topology/VectorBundle/Riemannian.lean