cardQuot_mul — Mathlib

English

For IsDedekindDomain S and modules over ℤ, the norm of the product of two ideals equals the product of their norms: cardQuot(I J) = cardQuot(I) cardQuot(J).

Русский

Для области Дедекнда S верно: cardQuot(I J) = cardQuot(I) · cardQuot(J).

LaTeX

$$$[\\text{IsDedekindDomain } S] \\rightarrow \\forall \\text{I,J : Ideal } S,\\; \\operatorname{cardQuot}(I J) = \\operatorname{cardQuot}(I) \\operatorname{cardQuot}(J)$$$

Lean4

/-- Multiplicativity of the ideal norm in number rings. -/
theorem cardQuot_mul [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S) :
    cardQuot (I * J) = cardQuot I * cardQuot J :=
  by
  let b := Module.Free.chooseBasis ℤ S
  haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective
  exact
    UniqueFactorizationMonoid.multiplicative_of_coprime cardQuot I J (cardQuot_bot _ _)
      (fun {I J} hI => by simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top])
      (fun {I} i hI =>
        have : Ideal.IsPrime I := Ideal.isPrime_of_prime hI
        cardQuot_pow_of_prime hI.ne_zero)
      fun {I J} hIJ =>
      cardQuot_mul_of_coprime <|
        Ideal.isCoprime_iff_sup_eq.mpr
          (Ideal.isUnit_iff.mp (hIJ (Ideal.dvd_iff_le.mpr le_sup_left) (Ideal.dvd_iff_le.mpr le_sup_right)))

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