isArtinian_iff — Mathlib

English

For a linear equivalence f: M ≃ₗ[R] P, IsArtinian R M holds if and only if IsArtinian R P holds.

Русский

Для линейного эквивалента f: M ≃ₗ[R] P верно, что M артинанов тогда и только тогда, когда P артинанов.

LaTeX

$$$IsArtinian\\ R\\ M \\iff IsArtinian\\ R\\ P$$$

Lean4

theorem isArtinian_iff (f : M ≃ₗ[R] P) : IsArtinian R M ↔ IsArtinian R P :=
  ⟨fun _ ↦ isArtinian_of_linearEquiv f, fun _ ↦ isArtinian_of_linearEquiv f.symm⟩
    -- This was previously a global instance,
    -- but it doesn't appear to be used and has been implicated in slow typeclass resolutions.

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