coe_inl

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.coe_inl

English

The product of the first and second projection maps is the identity morphism on A × B.

Русский

Произведение первых проекции fst и snd равно тождественному морфизму на A × B.

LaTeX

$$$\text{prod}(\text{fst } R A B)(\text{snd } R A B) = 1$$$

Lean4

@[simp]
theorem coe_inl : (inl R A B : A → A × B) = fun x => (x, 0) :=
  rfl

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

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

Разделы

Аффилиация

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