quotQuotEquivQuotOfLE_quotQuotMk — Mathlib

English

For ideals I ≤ J, the quotient-level equivalence quotQuotEquivQuotOfLE commutes with the quotient map quotQuotMk I J: applying the equivalence to a representative x yields the same result as taking x mod J.

Русский

Для I ≤ J, совпадение quotQuotEquivQuotOfLE и отображение quotQuotMk I J согласованы: результат применения эквивалентности к представителю x совпадает с x по модулю J.

LaTeX

$$$\quotQuotEquivQuotOfLE(h) (\quotQuotMk I J(x)) = (\Ideal.Quotient.mk J)(x) \quad\text{for } x\in R, \; h: I\le J$$$

Lean4

@[simp]
theorem quotQuotEquivQuotOfLE_quotQuotMk (x : R) (h : I ≤ J) :
    quotQuotEquivQuotOfLE h (quotQuotMk I J x) = (Ideal.Quotient.mk J) x :=
  rfl

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