Theorems · Definition · commutative algebra

Ideal.quotientEquivAlgOfEq

(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] → I = J → (A ⧸ I) ≃ₐ[R₁] A ⧸ J

Quotienting by equal ideals gives equivalent algebras.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

23 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebraIdeal.IsTwoSidedIdeal.IsTwoSided