isRegular_congr' — Mathlib

English

If e is a σ-ring-linear equivalence and rs is a list in R, then IsRegular M rs ⇔ IsRegular M₂ (rs.map σ).

Русский

Если e — σ-линейное эквивалентное отображение и rs — список в R, то 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.isRegular_congr' (e : M ≃ₛₗ[σ] M₂) (rs : List R) :
    IsRegular M rs ↔ IsRegular M₂ (rs.map σ) :=
  e.toAddEquiv.isRegular_congr <| List.forall₂_map_right_iff.mpr <| List.forall₂_same.mpr fun r _ x => e.map_smul' r x

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