isStarNormal_inr

Mathlib.Algebra.Algebra.Unitization

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

← MathLib Explorer

English

IsStarNormal is preserved under inr embedding.

Русский

IsStarNormal сохраняется при вложении inr.

LaTeX

$$IsStarNormal_inr : IsStarNormal a → IsStarNormal (a : Unitization R A)$$

Lean4

@[simp]
theorem isStarNormal_inr : IsStarNormal (a : Unitization R A) ↔ IsStarNormal a := by
  simp only [isStarNormal_iff, commute_iff_eq, ← inr_star, ← inr_mul, inr_injective.eq_iff]

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

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

Разделы

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

Аффилиация

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