Theorem FunctionField.algebraMap_injective

Modification history

2026-05-06 16:04
Mathlib/NumberTheory/FunctionField.lean
feat(FunctionField): constant extensions are finite (#37388) …
Modified FunctionField.algebraMap_injectiveView on Github →
2026-04-11 14:19
Mathlib/NumberTheory/FunctionField.lean
chore(FunctionField): rename vars when constant field is not nec. finite (#37894) …
Modified FunctionField.algebraMap_injectiveView on Github →
2025-03-03 16:46
Mathlib/NumberTheory/FunctionField.lean
chore(NumberTheory/FunctionField): rename `algebraMap_injective` to `FunctionField.algebraMap_injective` (#22489) …
Added FunctionField.algebraMap_injectiveView on Github →