of_mul_unit

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.IsIntegralElem.of_mul_unit

← MathLib Explorer

English

There is an instance: Algebra.IsIntegral R[X] S[X] given the IsIntegral data for R,S.

Русский

Существует экземпляр: Algebra.IsIntegral R[X] S[X], если есть IsIntegral для R и S.

LaTeX

$$$Algebra.IsIntegral R[X] S[X]$$$

Lean4

theorem of_mul_unit (x y : S) (r : R) (hr : f r * y = 1) (hx : f.IsIntegralElem (x * y)) : f.IsIntegralElem x :=
  letI : Algebra R S := f.toAlgebra
  IsIntegral.of_mul_unit hr hx

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

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

Разделы

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

Аффилиация

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