coeff_toSubring' — Mathlib

English

A variant of coeff_toSubring asserting equality of coefficients under the same construction in a slightly different form.

Русский

Вариант утверждения о равенстве коэффициентов в той же конструционности.

LaTeX

$$$(\\operatorname{coeff}((\\mathrm{toSubring}\\ p\\ T\\ hp)\\ n)).1 = \\operatorname{coeff}\\ p\\ n$$$

Lean4

theorem coeff_toSubring' {n : ℕ} : (coeff (toSubring p T hp) n).1 = coeff p n := by simp

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