Commit 2025-05-13 21:29 87a50461

View on Github →

chore: fix spelling mistakes (#24857)

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Modified Mathlib/Order/Filter/Pi.lean

Modified Mathlib/Tactic/Ring/RingNF.lean

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

Modified scripts/zulip_emoji_reactions.py