starMap_id — Mathlib

English

starMap preserves identity: starMap of the identity nonunital star algebra hom equals the identity on the unitization.

Русский

starMap сохраняет единичный отображение: starMap(идентичности) = идентичность единичизации.

LaTeX

$$$\text{starMap}(\mathrm{NonUnitalStarAlgHom.id}) = \mathrm{StarAlgHom.id}$$$

Lean4

/-- `starMap` is functorial:
`starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)`. -/
@[simp]
theorem starMap_id : starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B) := by ext; all_goals simp

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