coe_chainTop — Mathlib

English

The chainTop value is exactly chainTopCoeff α β times α plus β, in function form.

Русский

Значение chainTop равно chainTopCoeff α β, умноженному на α, плюс β, в виде функции.

LaTeX

$$$ (\\text{chainTop} α β) = (\\text{chainTopCoeff}(α, β) : \\mathbb{Z}) · α + β $$$

Lean4

@[simp]
theorem coe_chainTop : (chainTop α β : L → R) = (chainTopCoeff α β : ℤ) • α + β := by rw [Nat.cast_smul_eq_nsmul ℤ]; rfl

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