map_inv — Mathlib

English

If I is a principal fractional ideal and I ≠ 0, then I I^{-1} = 1.

Русский

Если I является порожденным дробным идеалом и I ≠ 0, то I I^{-1} = 1.

LaTeX

$$$$\text{If } I \text{ is principal and } I \neq 0,\; I \cdot I^{-1} = 1.$$$$

Lean4

@[simp]
protected theorem map_inv (I : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') : I⁻¹.map (h : K →ₐ[R₁] K') = (I.map h)⁻¹ := by
  rw [inv_eq, FractionalIdeal.map_div, FractionalIdeal.map_one, inv_eq]

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