of_finite_quot_finite_ideal

Mathlib.RingTheory.Ideal.Quotient.Basic

URI: https://scilib.ai/kg/mathlib#Finite.of_finite_quot_finite_ideal

← MathLib Explorer

English

If I is a finite ideal and the quotient R/I is finite, then R is finite.

Русский

Если I конечен, и фактор-кольцо R/I конечно, то R конечно.

LaTeX

$$Finite R$$

Lean4

theorem _root_.Finite.of_finite_quot_finite_ideal [hI : Finite I] [h : Finite (R ⧸ I)] : Finite R :=
  @Finite.of_finite_quot_finite_addSubgroup _ _ _ hI h

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

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

Разделы

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

Аффилиация

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