algebraMap_mk'

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

URI: https://scilib.ai/kg/mathlib#IsIntegralClosure.algebraMap_mk'

English

mk' respects equality: if x = x', then mk'(A, x, hx) = mk'(A, x', hx').

Русский

mk' сохраняет равенство: если x = x', то mk'(A, x, hx) = mk'(A, x', hx').

LaTeX

$$$x = x' \Rightarrow \ mk'(A, x, hx) = mk'(A, x', hx')$$$

Lean4

@[simp]
theorem algebraMap_mk' (x : B) (hx : IsIntegral R x) : algebraMap A B (mk' A x hx) = x :=
  Classical.choose_spec (isIntegral_iff.mp hx)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru