instIsStarNormal

Mathlib.Algebra.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.instIsStarNormal

English

An instance making inr a star normal element is inherited from a.

Русский

Экземпляр, задающий inr как звездно-нормальный элемент, унаследуется от a.

LaTeX

$$IsStarNormal(Unitization.inr a)$$

Lean4

instance instIsStarNormal (a : A) [IsStarNormal a] : IsStarNormal (a : Unitization R A) :=
  isStarNormal_inr.mpr ‹_›

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

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

Разделы

Аффилиация

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