English
Let a,b be elements of a ring-like structure with compatible scalar actions on a module M. Then a·b and b·a are M-regular if and only if a and b are M-regular. In particular, regularity of the products in both orders is equivalent to regularity of each factor.
Русский
Пусть a и b — элементы кольца с совместимыми действиями на модуль M. Тогда a·b и b·a являются M-регулярными тогда и только тогда, когда a и b самостоятельно являются M-регулярными. Регулярность произведений в обоих направлениях эквивалентна регулярности каждого множителя.
LaTeX
$$$\mathrm{IsSMulRegular}_M(a \cdot b) \; \land\; \mathrm{IsSMulRegular}_M(b \cdot a) \; \iff\; \mathrm{IsSMulRegular}_M(a) \land \mathrm{IsSMulRegular}_M(b)$$$
Lean4
/-- Two elements `a` and `b` are `M`-regular if and only if both products `a * b` and `b * a`
are `M`-regular. -/
theorem mul_and_mul_iff [Mul R] [IsScalarTower R R M] :
IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b :=
by
refine ⟨?_, ?_⟩
· rintro ⟨ab, ba⟩
exact ⟨ba.of_mul, ab.of_mul⟩
· rintro ⟨ha, hb⟩
exact ⟨ha.mul hb, hb.mul ha⟩
