rank_polynomial_polynomial — Mathlib

English

The rank is preserved under the passage to polynomial rings in both base and target rings: rank_R[X](S[X]) = rank_R(S).

Русский

Сохранение ранга при переходе к полиномиальным колцам в обоих основаниях и целевых кольцах: rank_{R[X]}(S[X]) = rank_R(S).

LaTeX

$$$\operatorname{Module.rank}\,R[X]\,S[X] = \operatorname{Module.rank}\,R\,S$$$

Lean4

theorem rank_polynomial_polynomial : Module.rank R[X] S[X] = Module.rank R S :=
  ((Algebra.isPushout_iff ..).mp inferInstance).rank_eq

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