and_of_mul_of_mul — Mathlib

English

If IsRegular (a*b) and IsRegular (b*a), then IsRegular a and IsRegular b.

Русский

Если IsRegular(a*b) и IsRegular(b*a), то IsRegular a и IsRegular b.

LaTeX

$$IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b$$

Lean4

/-- The "most used" implication of `mul_and_mul_iff`, with split hypotheses, instead of `∧`. -/
@[to_additive /-- The "most used" implication of `add_and_add_iff`, with split
    hypotheses, instead of `∧`. -/
    ]
theorem and_of_mul_of_mul (ab : IsRegular (a * b)) (ba : IsRegular (b * a)) : IsRegular a ∧ IsRegular b :=
  isRegular_mul_and_mul_iff.mp ⟨ab, ba⟩

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