isAssociatedPrime_iff — Mathlib

English

Associated primes are preserved under linear isomorphisms: if l: M ≃ₗ[R] M' is a linear equivalence, then I is associated prime for M iff it is for M'.

Русский

Ассоциированные простые сохраняются под линейными изоморфизмами: если l: M ≃ₗ[R] M' — линейное эквивалентность, то I ассоциирован в M тогда и только тогда, когда I ассоциирован в M'.

LaTeX

$$$$\forall l:\, M \cong M',\ IsAssociatedPrime I M \iff IsAssociatedPrime I M'. $$$$

Lean4

theorem isAssociatedPrime_iff (l : M ≃ₗ[R] M') : IsAssociatedPrime I M ↔ IsAssociatedPrime I M' :=
  ⟨fun h => h.map_of_injective l l.injective, fun h => h.map_of_injective l.symm l.symm.injective⟩

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