inr_apply_unit

Mathlib.Algebra.GroupWithZero.ProdHom

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

← MathLib Explorer

English

For x in G₀ˣ × H₀ˣ, inr maps to the second component: inr(x) = (1,x).

Русский

Для x ∈ G₀ˣ × H₀ˣ, inr отображает во вторую компоненту: inr(x) = (1,x).

LaTeX

$$$inr\; x = (1, x)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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