inhabited

Mathlib.Algebra.Homology.LocalCohomology

URI: https://scilib.ai/kg/mathlib#localCohomology.SelfLERadical.inhabited

English

There is a canonical cast morphism between self-le radical objects when radicals match.

Русский

Существует каноническое отображение-приведение между объектами SelfLERadical при совпадении радикалов.

LaTeX

$$$\\text{SelfLERadical.cast } hJK : J \\leadsto K$$$

Lean4

instance inhabited (J : Ideal R) : Inhabited (SelfLERadical J) where default := ⟨J, Ideal.le_radical⟩

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

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

Разделы

Аффилиация

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