English
The Pi-type isQuasiregular property holds iff it holds coordinatewise: IsQuasiregular x ↔ ∀ i, IsQuasiregular (x i).
Русский
Свойство IsQuasiregular для функции на произведении равно сумме по координатам: IsQuasiregular x ⇔ ∀ i, IsQuasiregular (x i).
LaTeX
$$$\operatorname{IsQuasiregular}(x) \;\iff\; \forall i, \operatorname{IsQuasiregular}(x(i))$$$
Lean4
/-- The equivalence between pre-quasiregular elements of a product and the product of
pre-quasiregular elements. -/
def toProd [NonUnitalSemiring A] [NonUnitalSemiring B] :
PreQuasiregular (A × B) ≃* PreQuasiregular A × PreQuasiregular B
where
toFun := fun p => ⟨.mk p.val.1, .mk p.val.2⟩
invFun := fun ⟨a, b⟩ => .mk ⟨a.val, b.val⟩
map_mul' _ _ := rfl
