inl_apply_unit

Mathlib.Algebra.GroupWithZero.ProdHom

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

← MathLib Explorer

English

For x in G₀ˣ, fst(x) equals x’s first component.

Русский

Для x ∈ G₀ˣ, fst(x) равняется первой компоненте x.

LaTeX

$$$fst\; x = x.fst$$$

Lean4

@[simp]
theorem inl_apply_unit [DecidablePred fun x : G₀ ↦ x = 0] (x : G₀ˣ) :
    inl G₀ H₀ x = ((x, (1 : H₀ˣ)) : WithZero (G₀ˣ × H₀ˣ)) := by simp [inl]

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

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

Разделы

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

Аффилиация

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