Def FunctionField.inftyValuedFqt

Modification history

2026-04-14 14:26
Mathlib/NumberTheory/FunctionField.lean
chore(FunctionField): move `inftyValuation` and `FqtInfty` to `RatFunc` namespace (#38030) …
Deleted FunctionField.inftyValuedFqtView 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.inftyValuedFqtView on Github →
2025-07-04 09:20
Mathlib/NumberTheory/FunctionField.lean
feat(WithZero): `exp : ℤ → ℤᵐ⁰`, `log : ℤᵐ⁰ → ℤ` (#24977) …
Modified FunctionField.inftyValuedFqtView on Github →
2023-06-21 07:53
Mathlib/NumberTheory/FunctionField.lean
feat: port NumberTheory.FunctionField (#5332)
Added FunctionField.inftyValuedFqtView on Github →