fst_comp_inl

Mathlib.Algebra.GroupWithZero.ProdHom

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.fst_comp_inl

English

The composition fst ∘ inl equals the identity on G₀.

Русский

Композиция fst ∘ inl равна тождеству на G₀.

LaTeX

$$$(fst \,.\, inl) = id$$$

Lean4

@[simp]
theorem fst_comp_inl [DecidablePred fun x : G₀ ↦ x = 0] : (fst ..).comp (inl G₀ H₀) = .id _ :=
  MonoidWithZeroHom.ext fun _ ↦ fst_inl _

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

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

Разделы

Аффилиация

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