Nonzerodivisors under multiplicative isomorphisms

A multiplicative isomorphism e : R ≃* S, for instance a ring isomorphism, preserves and reflects the elements whose left multiplication is injective: a is IsSMulRegular in R if and only if e a is in S (TauCeti.isSMulRegular_map_iff). This specializes Mathlib's Equiv.isSMulRegular_congr to an element acting on its own ring, where the compatibility hypothesis is map_mul.

@[simp]

theorem TauCeti.isSMulRegular_map_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [Mul R] [Mul S] [EquivLike F R S] [MulEquivClass F R S] (e : F) (a : R) : IsSMulRegular S (e a) ↔ IsSMulRegular R a

A multiplicative isomorphism preserves and reflects nonzerodivisors: e a is a nonzerodivisor of S if and only if a is one of R.