length_eq — Mathlib

English

If e: M ≃ₗ[R] N is a linear isomorphism, then Module.length R M = Module.length R N.

Русский

Если e: M ≃ₗ[R] N — линейный изоморфизм, то длина модулей совпадает: длина M равна длине N.

LaTeX

$$$\operatorname{length}(R,M) = \operatorname{length}(R,N)\quad \text{for any } e : M \simeq_{R} N.$$$

Lean4

theorem length_eq {N : Type*} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.length R M = Module.length R N :=
  by
  apply WithBot.coe_injective
  rw [Module.coe_length, Module.coe_length, Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap e)]

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