isEmptyRingEquiv_eq_coeff_zero — Mathlib

English

For any x in MvPolynomial σ R, isEmptyRingEquiv R σ x equals the coefficient at 0 of x.

Русский

Для любого x∈MvPolynomial σ R отображение isEmptyRingEquiv R σ x равно коэффициенту при 0 в x.

LaTeX

$$$\text{isEmptyRingEquiv} \;R\;\sigma\;x = \operatorname{coeff}_0(x)$$$

Lean4

theorem isEmptyRingEquiv_eq_coeff_zero {σ R : Type*} [CommSemiring R] [IsEmpty σ] {x} :
    isEmptyRingEquiv R σ x = x.coeff 0 := by obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x; simp

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