lift_root — Mathlib

English

Let R,S be commutative rings, f ∈ R[X], i : R →+* S, and a ∈ S with f.eval₂ i a = 0. Then the universal lifting map sends root f to a: lift i a h (root f) = a.

Русский

Пусть R, S — коммутативные кольца, f ∈ R[X], i : R →+* S, и a ∈ S удовлетворяют f.eval₂ i a = 0. Тогда универсальный подъем отображения отправляет корень f в a: lift i a h (root f) = a.

LaTeX

$$$lift\\ i\\ a\\ h\\ (\\text{root } f) = a$$$

Lean4

@[simp]
theorem lift_root : lift i a h (root f) = a := by rw [root, lift_mk, eval₂_X]

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