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.