prodMk

Mathlib.Algebra.Regular.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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