Skip to content

fix(pitfalls.md): remove repeated word#760

Merged
grunweg merged 5 commits intoleanprover-community:lean4from
AxelBoldt:lean4
Dec 8, 2025
Merged

fix(pitfalls.md): remove repeated word#760
grunweg merged 5 commits intoleanprover-community:lean4from
AxelBoldt:lean4

Conversation

@AxelBoldt
Copy link
Contributor

In pitfalls.md / Distance in Fin n → ℝ, in the sentence

To instead use the standard Euclidean metric (also called the $L^2$ metric), you must use instead use EuclideanSpace ℝ (Fin n)

I removed the double "use" and the double "instead".

@grunweg grunweg changed the title Removed "use instead" in pitfalls.md / Distance in Fin n → ℝ fix(pitfalls.md): remove repeated word Dec 8, 2025
@grunweg
Copy link
Contributor

grunweg commented Dec 8, 2025

Thanks!

@grunweg grunweg merged commit c55817d into leanprover-community:lean4 Dec 8, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants