unitization_apply

Mathlib.Algebra.Algebra.Subalgebra.Unitization

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.unitization_apply

English

Another auxiliary statement used in the proof of unitization equivalence.

Русский

Другое вспомогательное утверждение, используемое в доказательстве эквивалентности единизации.

LaTeX

$$Auxiliary step$$

Lean4

@[simp]
theorem unitization_apply (x : Unitization R s) : unitization s x = algebraMap R A x.fst + x.snd :=
  rfl

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

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

Разделы

Аффилиация

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