Theorems · Theorem · ring theory

Algebra.IsCentral.of_algEquiv

∀ (K : Type u) [inst : CommSemiring K] (D D' : Type v) [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [h : Algebra.IsCentral K D] [inst_3 : Semiring D'] [inst_4 : Algebra K D'] (e : D ≃ₐ[K] D'), Algebra.IsCentral K D'

Defined in

Mathlib.Algebra.Central.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraAlgebra.IsCentralSemiringAlgebra