Theorems · Theorem · commutative algebra

Ideal.quotientEquivAlgOfEq_symm

∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J),
  (Ideal.quotientEquivAlgOfEq R₁ h).symm = Ideal.quotientEquivAlgOfEq R₁ ⋯

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebraIdeal.IsTwoSidedIdeal.IsTwoSided