isWeaklyRegular_congr — Mathlib

English

If there is a σ-linear equivalence e between M and M₂, then IsRegular M rs holds iff IsRegular M₂ (rs.map σ).

Русский

Если существует σ-линейное эквивалентное отображение между M и M₂, то IsRegular M rs выполняется тогда и только тогда, когда IsRegular M₂ (rs.map σ).

LaTeX

$$$\\forall e:\\, M \\simeq_\\sigma M_2,\\; rs:\\; IsRegular(M, rs) \\iff IsRegular(M_2, rs^{\\sigma})$$$

Lean4

theorem _root_.LinearEquiv.isWeaklyRegular_congr [Module R M₂] (e : M ≃ₗ[R] M₂) (rs : List R) :
    IsWeaklyRegular M rs ↔ IsWeaklyRegular M₂ rs :=
  Iff.trans (e.isWeaklyRegular_congr' rs) <| iff_of_eq <| congrArg _ rs.map_id

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