cardQuot_mul_of_coprime — Mathlib

English

Multiplicity of the ideal norm for coprime ideals: cardQuot(I ∙ J) = cardQuot(I) ∙ cardQuot(J).

Русский

Множество нормы идеалов для попарно взаимно простых идеалов: cardQuot(IJ) = cardQuot(I)·cardQuot(J).

LaTeX

$$cardQuot(I * J) = cardQuot(I) * cardQuot(J)$$

Lean4

/-- Multiplicity of the ideal norm, for coprime ideals.
This is essentially just a repackaging of the Chinese Remainder Theorem.
-/
theorem cardQuot_mul_of_coprime {I J : Ideal S} (coprime : IsCoprime I J) :
    cardQuot (I * J) = cardQuot I * cardQuot J := by
  rw [cardQuot_apply, cardQuot_apply, cardQuot_apply,
    Nat.card_congr (Ideal.quotientMulEquivQuotientProd I J coprime).toEquiv, Nat.card_prod]

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