isQuasiregular_prod_iff — Mathlib

English

For nonunital semirings A,B, IsQuasiregular on x is equivalent to IsUnit of x in Prod.

Русский

IsQuasiregular на паре эквивалентно единичности на произведении.

LaTeX

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

Lean4

theorem isQuasiregular_prod_iff [NonUnitalSemiring A] [NonUnitalSemiring B] (a : A) (b : B) :
    IsQuasiregular (⟨a, b⟩ : A × B) ↔ IsQuasiregular a ∧ IsQuasiregular b :=
  by
  simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toProd A B), Prod.isUnit_iff]
  congr!

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