Theorems · Theorem · commutative algebra

Ideal.quotEquivOfEq_mk

∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I = J) (x : R),
  (Ideal.quotEquivOfEq h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x

Defined in

Mathlib.RingTheory.Ideal.Quotient.Defs

Cited by

3 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingIdeal.IsTwoSidedIdeal.IsTwoSided