ringKrullDim_eq_of_ringEquiv — Mathlib

English

If R ≃+* S is a ring isomorphism, then ringKrullDim R = ringKrullDim S.

Русский

Если кольца R и S изоморфны как кольца, то их ringKrullDim равны.

LaTeX

$$$ringKrullDim R = ringKrullDim S$$$

Lean4

/-- If `R` and `S` are isomorphic, then `ringKrullDim R = ringKrullDim S`. -/
theorem ringKrullDim_eq_of_ringEquiv (e : R ≃+* S) : ringKrullDim R = ringKrullDim S :=
  le_antisymm (ringKrullDim_le_of_surjective e.symm e.symm.surjective) (ringKrullDim_le_of_surjective e e.surjective)

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