isRightRegular_mk — Mathlib

English

For R,S with multiplications, IsRightRegular (a,b) holds iff IsRightRegular a and IsRightRegular b.

Русский

Для пары (a,b) верно: IsRightRegular (a,b) ⇔ IsRightRegular a ∧ IsRightRegular b.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem isRightRegular_mk {a : R} {b : S} : IsRightRegular (a, b) ↔ IsRightRegular a ∧ IsRightRegular b :=
  have : Nonempty R := ⟨a⟩;
  have : Nonempty S := ⟨b⟩;
  Iff.symm <| Prod.map_injective |>.symm

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