doc: adjust file reference in Data.Sum

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

doc: adjust file reference in Data.Sum #6158

Closed b-mehta closed 4 days ago

b-mehta commented 4 days ago

This file was upstreamed from batteries; I just got bitten by the invalid reference and it took quite a while to figure out that this one had been moved!

leanprover-community-bot commented 4 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-21 18:01:27)