fst_comp_inl

Mathlib.Algebra.Order.GroupWithZero.Lex

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

English

A lemma expressing the simplification of fst after inl in Lex context.

Русский

Лемма упрощения fst после inl в контексте Lex.

LaTeX

$$$(fst\circ inl) = id$$$

Lean4

@[simp]
theorem fst_comp_inl : (fst _ _).comp (inl α β) = .id α :=
  by
  ext x
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;> simp

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

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

Разделы

Аффилиация

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