lift_algEquiv — Mathlib

English

If h and h' are IsAdjoinRoot data for the same f, then lifting through i preserves the comparison with the Algebra homomorphism; concretely, h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z.

Русский

Если данные IsAdjoinRoot для одного f совпадают, то переход через i сохраняет совместимость с алгебраическим изоморфизмом.

LaTeX

$$h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z$$

Lean4

@[simp]
theorem lift_algEquiv (i : R →+* U) (x hx z) : h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by
  rw [← h.map_repr z]; simp [-map_repr]

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