isIntegral_respectsIso

Mathlib.RingTheory.RingHom.Integral

URI: https://scilib.ai/kg/mathlib#RingHom.isIntegral_respectsIso

← MathLib Explorer

English

Integral property respects isomorphisms: IsIntegral is preserved under isomorphisms.

Русский

Интегральность сохраняется под изоморфизмами.

LaTeX

$$$\\text{RespectsIso}(\\text{IsIntegral})$$$

Lean4

theorem isIntegral_respectsIso : RespectsIso fun f => f.IsIntegral :=
  by
  apply isIntegral_stableUnderComposition.respectsIso
  introv x
  rw [← e.apply_symm_apply x]
  apply RingHom.isIntegralElem_map

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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