isRegular_mk

Mathlib.Algebra.Regular.Prod

URI: https://scilib.ai/kg/mathlib#Prod.isRegular_mk

← MathLib Explorer

English

The pair (a,b) is regular if and only if a and b are regular.

Русский

Пара (a,b) регулярна тогда и только тогда, когда a и b регулярны.

LaTeX

$$IsRegular( { fst := a, snd := b } ) \iff IsRegular a ∧ IsRegular b$$

Lean4

@[to_additive (attr := simp)]
theorem isRegular_mk {a : R} {b : S} : IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b := by
  simp [isRegular_iff, and_and_and_comm]

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

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

Разделы

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

Аффилиация

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