inr_apply

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#NonUnitalStarAlgHom.inr_apply

English

For x ∈ B, inr x = (0, x).

Русский

Для x ∈ B, inr x = (0, x).

LaTeX

$$$ inr R A B x = (0, x) $$$

Lean4

theorem inr_apply (x : B) : inr R A B x = (0, x) :=
  rfl

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

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

Разделы

Аффилиация

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