ofFinsupp_inj — Mathlib

English

The embedding that sends a ∈ AddMonoidAlgebra R Nat to ⟨a⟩ ∈ R[X] is injective; equivalently, if ⟨a⟩ = ⟨b⟩ then a = b.

Русский

Встраивание a ∈ AddMonoidAlgebra R Nat в R[X] через ⟨a⟩ инъективно; то есть если ⟨a⟩ = ⟨b⟩, то a = b.

LaTeX

$$$(\langle a \rangle : R[X]) = \langle b \rangle \iff a = b$$$

Lean4

/-- A more convenient spelling of `Polynomial.ofFinsupp.injEq` in terms of `Iff`. -/
theorem ofFinsupp_inj {a b} : (⟨a⟩ : R[X]) = ⟨b⟩ ↔ a = b :=
  iff_of_eq (ofFinsupp.injEq _ _)

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