height_map — Mathlib

English

For a ring isomorphism e, the height of the mapped ideal equals the height of the original ideal.

Русский

При изоморфизме кольца высота образа идеала равна высоте исходного идеала.

LaTeX

$$$\operatorname{height}(I \mapsto I.e) = \operatorname{height}(I).$$$

Lean4

@[simp]
theorem height_map {S : Type*} [CommRing S] (e : R ≃+* S) (I : Ideal R) : (I.map e).height = I.height := by
  rw [← Ideal.comap_symm e, height_comap]

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