finite_containsIdentities

Mathlib.RingTheory.RingHom.Finite

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

English

Finite contains identities for ring morphisms.

Русский

Конечность содержит единицы для колец.

LaTeX

$$$\\operatorname{ContainsIdentities}(\\text{Finite})$$$

Lean4

theorem finite_containsIdentities : ContainsIdentities @Finite :=
  Finite.id

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

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

Разделы

Аффилиация

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