Theorems · Inductive type · ring theory

AlgEquiv

(R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → Type (max v w)

An equivalence of algebras (denoted as A ≃ₐ[R] B) is an equivalence of rings commuting with the actions of scalars.

Defined in

Mathlib.Algebra.Algebra.Equiv

Cited by

1,681 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra