mul_iff — Mathlib

English

A product is M-regular if and only if its factors are M-regular.

Русский

Произведение является M-регулярным тогда и только тогда, когда каждый множитель M-регулярен.

LaTeX

$$$IsSMulRegular M (a b) \iff IsSMulRegular M a \land IsSMulRegular M b$$$

Lean4

/-- A product is `M`-regular if and only if the factors are. -/
theorem mul_iff : IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b :=
  by
  rw [← mul_and_mul_iff]
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

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