isSMulRegular_congr — Mathlib

English

A linear equivalence e gives an equivalence of the IsSmulRegular property for corresponding r.

Русский

Линейное эквивалентное отображение задаёт эквивалентность регулярности для соответствующих r.

LaTeX

$$$IsSMulRegular\;M\;r \iff IsSMulRegular\;N\; r$ under a suitable LinearEquiv.$$

Lean4

theorem isSMulRegular_congr [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (r : R) :
    IsSMulRegular M r ↔ IsSMulRegular N r :=
  e.isSMulRegular_congr' r

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