English
If e is a σ-linear equivalence, then IsRegular M rs ↔ IsRegular M₂ (rs.map σ).
Русский
Если e — σ-линейное эквивалентное отображение между 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_.AddEquiv.isRegular_congr {e : M ≃+ M₂} {as bs}
(h : List.Forall₂ (fun (r : R) (s : S) => ∀ x, e (r • x) = s • e x) as bs) : IsRegular M as ↔ IsRegular M₂ bs :=
by
conv => congr <;> rw [isRegular_iff, ne_eq, eq_comm, ← subsingleton_quotient_iff_eq_top]
let e' := QuotientAddGroup.congr _ _ e <| AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective h
exact and_congr (e.isWeaklyRegular_congr h) e'.subsingleton_congr.not
