RatFuncAdicCompl — Mathlib

English

An abbreviation RatFuncAdicCompl denotes the X-adic completion of RatFunc K, i.e., the adic completion of RatFunc K with respect to the ideal generated by X.

Русский

Обозначение RatFuncAdicCompl обозначает X-адическое дополнение RatFunc K, то есть адикальное дополнение RatFunc K по идеалу, порождаемому X.

LaTeX

$$$\mathrm{RatFuncAdicCompl} = \operatorname{adicCompletion}(\mathrm{RatFunc}\,K, \mathrm{idealX}(K))$$$

Lean4

/-- An abbreviation for the `X`-adic completion of `RatFunc K` -/
abbrev RatFuncAdicCompl :=
  adicCompletion (RatFunc K)
    (idealX K)
      /- The two instances below make `comparePkg` and `comparePkg_eq_extension` slightly faster. -/

Похожие утверждения