quotientMulEquivQuotientProd_fst — Mathlib

English

Second projection of quotientMulQuotientProd matches the corresponding factor map to R/J.

Русский

Вторая компонента отображения совпадает с факторной проекцией к R/J.

LaTeX

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

Lean4

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

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