algEquivOfAlgEquiv_eq_map — Mathlib

English

If M maps to T under h, the corresponding algebra equivalence sends algebraMap_R^S x to algebraMap_P^Q h x.

Русский

Если M отображается в T через h, соответствующее алгебровое эквивалентное отображение отправляет algebraMap_R^S x в algebraMap_P^Q h x.

LaTeX

$$$\\text{algEquivOfAlgEquiv}(S,Q,h,H)(\\mathrm{algebraMap}_R^S x) = \\mathrm{algebraMap}_P^Q (h x)$$$

Lean4

theorem algEquivOfAlgEquiv_eq_map :
    (algEquivOfAlgEquiv S Q h H : S →+* Q) = map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) :=
  rfl

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