coeIdeal_inf — Mathlib

English

If I and J are ideals of R, then the fractional ideal corresponding to their intersection is the intersection of the corresponding fractional ideals: ↑(I ∩ J) = ↑I ∩ ↑J.

Русский

Пусть I и J — идеалы кольца R. Соответствующий дробному идеалу пересечение удовлетворяет: ↑(I ∩ J) = ↑I ∩ ↑J.

LaTeX

$$$↑(I \cap J) = ↑I \cap ↑J$$$

Lean4

@[simp, norm_cast]
theorem coeIdeal_inf [FaithfulSMul R P] (I J : Ideal R) : (↑(I ⊓ J) : FractionalIdeal S P) = ↑I ⊓ ↑J :=
  by
  apply coeToSubmodule_injective
  exact Submodule.map_inf (Algebra.linearMap R P) (FaithfulSMul.algebraMap_injective R P)

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