isQuasiregular_pi_iff — Mathlib

English

For nonunital semirings A and B, IsQuasiregular on the pair (a,b) is equivalent to IsQuasiregular a and IsQuasiregular b.

Русский

Для произведения IsQuasiregular (a,b) эквивалентно IsQuasiregular a и IsQuasiregular b.

LaTeX

$$$IsQuasiregular(\langle a,b \rangle) \;\iff\; IsQuasiregular(a) \land IsQuasiregular(b)$$$

Lean4

theorem isQuasiregular_pi_iff [∀ i, NonUnitalSemiring (κ i)] (x : ∀ i, κ i) :
    IsQuasiregular x ↔ ∀ i, IsQuasiregular (x i) :=
  by
  simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]
  congr!

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