prodMk

Mathlib.Algebra.Regular.Prod

URI: https://scilib.ai/kg/mathlib#IsLeftRegular.prodMk

← MathLib Explorer

English

If a and b are left-regular, then the pair (a,b) is left-regular.

Русский

Если a и b лево-регулярны, то пара (a,b) лево-регулярна.

LaTeX

$$IsLeftRegular a \Rightarrow IsLeftRegular b \Rightarrow IsLeftRegular { fst := a, snd := b }$$

Lean4

@[to_additive]
theorem prodMk {a : R} {b : S} (ha : IsLeftRegular a) (hb : IsLeftRegular b) : IsLeftRegular (a, b) :=
  Prod.isLeftRegular_mk.2 ⟨ha, hb⟩

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

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

Разделы

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

Аффилиация

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