coe_inj

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.coe_inj

English

The embedding is faithful: φ mapped equals ψ mapped if and only if φ = ψ.

Русский

Встраивание сохраняет различие: если вложения равны, значит полиномы равны.

LaTeX

$$$(\\uparrow\\varphi) = \\uparrow\\psi \\;\\iff\\; \\varphi = \\psi$$$

Lean4

@[simp, norm_cast]
theorem coe_inj : (φ : MvPowerSeries σ R) = ψ ↔ φ = ψ :=
  (coe_injective σ R).eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru