support_eq — Mathlib

English

If e: M ≃_R N is a linear equivalence, then Supp_R(M) = Supp_R(N).

Русский

Если e: M ≃_R N — линейное эквивалентное отображение, опора модулей совпадает: Supp_R(M) = Supp_R(N).

LaTeX

$$Supp_R(M) = Supp_R(N) for e ∈ LinearEquiv(M,N)$$

Lean4

theorem support_eq (e : M ≃ₗ[R] N) : Module.support R M = Module.support R N :=
  (Module.support_subset_of_injective e.toLinearMap e.injective).antisymm
    (Module.support_subset_of_surjective e.toLinearMap e.surjective)

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