English
Coercions from polynomials to Laurent series are compatible: Coe (P:Polynomial F) via power-series embedding equals the natural RatFunc embedding.
Русский
Согласованы две цепочки приведения: полином → лорантовые ряды через вложение в РатФунк → лорантовые ряды; оба дают один и тот же результат.
LaTeX
$$$((P: F[X]) : F⟦X⟧)\!:\, F⸨X⸩ = P\,.$$$
Lean4
theorem coe_coe (P : Polynomial F) : ((P : F⟦X⟧) : F⸨X⸩) = (P : RatFunc F) := by
simp [coePolynomial, coe_def, ← IsScalarTower.algebraMap_apply]
-- Porting note: removed `norm_cast` because "badly shaped lemma, rhs can't start with coe"
-- even though `single 1 1` is a bundled function application, not a "real" coercion
