finite_iff_of_bijective — Mathlib

English

If a linear map f is bijective, then Module.Finite R M holds iff Module.Finite S P holds.

Русский

Если линейное отображение f биективно, то Module.Finite R M эквивалично Module.Finite S P.

LaTeX

$$LinearMap.finite_iff_of_bijective (f) (hf) : Module.Finite R M ↔ Module.Finite S P$$

Lean4

theorem _root_.LinearMap.finite_iff_of_bijective (f : M →ₛₗ[σ] P) (hf : Function.Bijective f) :
    Module.Finite R M ↔ Module.Finite S P :=
  ⟨fun _ ↦ of_surjective f hf.surjective, fun _ ↦
    ⟨fg_of_fg_map_injective f hf.injective <| by
        rwa [Submodule.map_top, LinearMap.range_eq_top.2 hf.surjective, ← Module.finite_def]⟩⟩

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