coe_mapIntegralClosure — Mathlib

English

The underlying element of the mapped integral closure corresponds to applying the isomorphism to the underlying element.

Русский

Пусть x принадлежит интегральному замыканию; образ через отображение эквивалентности соответствует применению изоморфизма к базовому элементу.

LaTeX

$$$(f.mapIntegralClosure x : S) = f (x : A)$$$

Lean4

@[simp]
theorem coe_mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S) (x : integralClosure R A) :
    (f.mapIntegralClosure x : S) = f (x : A) :=
  rfl

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