Skip to content

Commit ba83d54

Browse files
committed
chore(NumberTheory/FunctionField): fix misnamed deprecations (leanprover-community#39001)
5 deprecation from leanprover-community#38030 misspelled `FqtInfty` as `FtInfty`, which caused issues in a downstream project. This PR fixes these deprecations to have the correct name. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
1 parent 0d6aac3 commit ba83d54

1 file changed

Lines changed: 5 additions & 5 deletions

File tree

Mathlib/NumberTheory/FunctionField.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -180,22 +180,22 @@ alias inftyValuation.X_inv := RatFunc.inftyValuation.X_inv
180180
alias inftyValuation.polynomial := RatFunc.inftyValuation.polynomial
181181

182182
@[deprecated RatFunc.inftyValued (since := "2026-04-14")]
183-
alias inftyValuedFt := RatFunc.inftyValued
183+
alias inftyValuedFqt := RatFunc.inftyValued
184184

185185
@[deprecated RatFunc.inftyValued.def (since := "2026-04-14")]
186-
alias inftyValuedFt.def := RatFunc.inftyValued.def
186+
alias inftyValuedFqt.def := RatFunc.inftyValued.def
187187

188188
@[deprecated RatFunc.CompletionAtInfty (since := "2026-04-14")]
189-
alias FtInfty := RatFunc.CompletionAtInfty
189+
alias FqtInfty := RatFunc.CompletionAtInfty
190190

191191
@[deprecated "Use the anonymous `Valued` instance on `RatFunc.CompletionAtInfty`"
192192
(since := "2026-04-14")]
193-
instance valuedFtInfty [DecidableEq F⟮X⟯] :
193+
instance valuedFqtInfty [DecidableEq F⟮X⟯] :
194194
Valued (RatFunc.CompletionAtInfty F) ℤᵐ⁰ :=
195195
inferInstance
196196

197197
@[deprecated RatFunc.valuedCompletionAtInfty.def (since := "2026-04-14")]
198-
alias valuedFtInfty.def := RatFunc.valuedCompletionAtInfty.def
198+
alias valuedFqtInfty.def := RatFunc.valuedCompletionAtInfty.def
199199

200200
end deprecated
201201

0 commit comments

Comments
 (0)