map_one_div — Mathlib

English

Under an algebra isomorphism h, the division of fractional ideals commutes with the map, i.e., map_h(I / J) = map_h(I) / map_h(J).

Русский

При изоморфизме алгебры h деление дробных идеалов сохраняется под отображением: map_h(I / J) = map_h(I) / map_h(J).

LaTeX

$$$ (I / J) map\ h = (I map\ h) / (J map\ h) $$$

Lean4

theorem map_one_div (I : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') : (1 / I).map (h : K →ₐ[R₁] K') = 1 / I.map h := by
  rw [FractionalIdeal.map_div, FractionalIdeal.map_one]

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