fst_inl

Mathlib.Algebra.GroupWithZero.ProdHom

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

← MathLib Explorer

English

For any x in G₀, fst (inl x) = x; inl embeds G₀ into the left factor.

Русский

Для любого x в G₀, fst(inl x) = x; inl внедряет G₀ в левый множитель.

LaTeX

$$$fst\; (inl\; x) = x$$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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