eval₂_repr_eq_eval₂_of_map_eq

English

Further compatibility: given e, (h.ofAlgEquiv e).algEquiv h'' equals e.symm.trans (h.algEquiv h'').

Русский

Дополнительная совместимость: существует равенство между преобразованиями изоморфизмов.

LaTeX

$$$(h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')$$$

Lean4

/-- Auxiliary lemma for `IsAdjoinRoot.lift` -/
theorem eval₂_repr_eq_eval₂_of_map_eq (z : S) (w : R[X]) (hzw : h.map w = z) : (h.repr z).eval₂ i x = w.eval₂ i x :=
  by
  rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw
  obtain ⟨y, hy⟩ := hzw
  rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

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