Commit 2025-03-03 16:46 2d6a6e65
View on Github →chore(NumberTheory/FunctionField): rename algebraMap_injective to FunctionField.algebraMap_injective (#22489)
Rename theorem algebraMap_injective to FunctionField.algebraMap_injective in file Mathlib/NumberTheory/FunctionField.lean. The theorem algebraMap_injective has always been in the root namespace before this PR.