starLift_symm_apply_apply

Mathlib.Algebra.Algebra.Unitization

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

English

The symmetry of the starLift construction relates φ and its inverse under unitization.

Русский

Симметрия конструирования starLift связывает φ и его обратное через единичизацию.

LaTeX

$$$\text{StarLift.symm}(φ)=\text{...}$$$

Lean4

@[simp high]
theorem starLift_symm_apply_apply (φ : Unitization R A →⋆ₐ[R] C) (a : A) : Unitization.starLift.symm φ a = φ a :=
  rfl

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

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

Разделы

Аффилиация

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