map_div — Mathlib

English

For a field isomorphism h between K and K', the image of a fractional division equals the division of images: map_h(I / J) = map_h(I) / map_h(J).

Русский

Пусть h — изоморфизм тел между K и K'. Тогда образ дробного деления сохраняется: map_h(I / J) = map_h(I) / map_h(J).

LaTeX

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

Lean4

@[simp]
protected theorem map_div (I J : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') :
    (I / J).map (h : K →ₐ[R₁] K') = I.map h / J.map h :=
  by
  by_cases H : J = 0
  · rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
  · simp [← coeToSubmodule_inj, div_nonzero H, div_nonzero (map_ne_zero _ H)]

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