fst_comp_inr — Mathlib

English

Let G and H be groups with zero. The first projection after the right injection into the product G × H is constant, sending every element of H to the multiplicative identity in G.

Русский

Пусть G и H — группы с нулём. Первая проекция после включения H в произведение G × H есть константное отображение, отправляющее каждый элемент H в единицу умножения в G.

LaTeX

$$$\forall h\in H_0,\ \mathrm{fst}(\mathrm{inr}(h)) = 1$$$

Lean4

@[simp]
theorem fst_comp_inr [DecidablePred fun x : H₀ ↦ x = 0] : (fst ..).comp (inr G₀ H₀) = 1 :=
  by
  ext x
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;> simp_all [WithZero.withZeroUnitsEquiv, fst, inr]

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