lift_root — Mathlib

English

Let h be an isAdjoinRoot for f inside S over R. For any algebra homomorphism i: R → T and any element x ∈ T with f(eval₂ i x) = 0, the lifting map sends the root of f to x, i.e., h.lift i x hx h.root = x.

Русский

Пусть h задаёт свойство IsAdjoinRoot для f над R внутри S. Пусть i : R → T — алгебраическая гомоморфия, и x ∈ T такая, что eval₂ i x(f) = 0. Тогда каноническое продолжение отображает корень f в x: h.lift i x hx h.root = x.

LaTeX

$$$ h.lift i x hx h.root = x $$$

Lean4

@[simp]
theorem lift_root : h.lift i x hx h.root = x := by rw [← h.map_X, lift_map, eval₂_X]

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