quotientMulEquivQuotientProd_snd — Mathlib

English

Second projection under the mul-based Chinese remainder is the left quotient factor.

Русский

Вторая проекция CRT для умножения равна левому фактору по квотам.

LaTeX

$$$\\text{snd}(I,J) = \\operatorname{Quotient.factor} \\; mul\\_le\_left$$$

Lean4

@[simp]
theorem quotientMulEquivQuotientProd_snd (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) :
    (quotientMulEquivQuotientProd I J coprime x).snd = Ideal.Quotient.factor mul_le_left x :=
  Quot.inductionOn x fun _ => rfl

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