isRegular_congr — Mathlib

English

If e is a LinearEquiv with RingHom.id R, then IsRegular M rs is equivalent to IsRegular M₂ rs.

Русский

Если e — линейное эквивалентности над R и тождественное отображение для кольца R, то IsRegular M rs эквивалентно IsRegular M₂ rs.

LaTeX

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

Lean4

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

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