Theorems · Definition · ring theory

Subalgebra.equivOfEq

{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S T : Subalgebra R A) → S = T → ↥S ≃ₐ[R] ↥T

Two subalgebras that are equal are also equivalent as algebras. This is the Subalgebra version of LinearEquiv.ofEq and Equiv.setCongr.

Defined in

Mathlib.Algebra.Algebra.Subalgebra.Basic

Cited by

15 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra