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.

Estimated changes