isWeaklyRegular_congr' — Mathlib

English

If e is a σ-linear equivalence between M and M₂, then IsWeaklyRegular M rs is equivalent to IsWeaklyRegular M₂ (rs mapped by σ).

Русский

Если e — линейное по σ тождество между M и M₂, то IsWeaklyRegular M rs эквивиentно IsWeaklyRegular M₂ (rs.map σ).

LaTeX

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

Lean4

theorem _root_.LinearEquiv.isWeaklyRegular_congr' (e : M ≃ₛₗ[σ] M₂) (rs : List R) :
    IsWeaklyRegular M rs ↔ IsWeaklyRegular M₂ (rs.map σ) :=
  e.toAddEquiv.isWeaklyRegular_congr <|
    List.forall₂_map_right_iff.mpr <| List.forall₂_same.mpr fun r _ x => e.map_smul' r x

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