isSMulRegular_congr — Mathlib

English

Under a compatible equivalence e: M ≃ M' and a relation between r and s, IsSMulRegular M r holds iff IsSMulRegular M' s.

Русский

При совместимой эквивалентности e: M ≃ M' и отношении между r и s, IsSMulRegular M r эквивалентно IsSMulRegular M' s.

LaTeX

$$Equiv.isSMulRegular_congr$$

Lean4

theorem isSMulRegular_congr {R S M M'} [SMul R M] [SMul S M'] {e : M ≃ M'} {r : R} {s : S}
    (h : ∀ x, e (r • x) = s • e x) : IsSMulRegular M r ↔ IsSMulRegular M' s :=
  (e.comp_injective _).symm.trans <| (iff_of_eq <| congrArg _ <| funext h).trans <| e.injective_comp _

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