theorem Module.length_eq_add_of_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (g : M →ₗ[R] P) (hg : Function.Surjective ⇑g) : length R M = length R P + length R ↥(LinearMap.ker g)

theorem Module.injective_of_eq_finite_length_of_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (g : M →ₗ[R] P) (hg : Function.Surjective ⇑g) (h : length R P ≠ ⊤) : length R M = length R P → Function.Injective ⇑g

theorem Module.bijective_of_eq_finite_length_of_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (g : M →ₗ[R] P) (hg : Function.Surjective ⇑g) (h : length R P ≠ ⊤) : length R M = length R P → Function.Bijective ⇑g

@[simp]

theorem Module.length_quot_restrictScalars (R : Type u_5) (S : Type u_6) (M : Type u_7) [Ring R] [AddCommGroup M] [Module R M] [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] (N : Submodule S M) : length R (M ⧸ Submodule.restrictScalars S N) = length R (M ⧸ N)

@[simp]

theorem Module.length_restrictScalars (R : Type u_5) (S : Type u_6) (M : Type u_7) [Ring R] [AddCommGroup M] [Module R M] [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] (N : Submodule S M) : length R ↥(Submodule.restrictScalars S N) = length R ↥N

theorem Module.length_le_of_tower (R : Type u_5) (S : Type u_6) (M : Type u_7) [Ring R] [AddCommGroup M] [Module R M] [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] : length S M ≤ length R M