Theorems · Theorem · ring theory

AlgEquiv.piCongrRight_symm

∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (A₁ i)] [inst_2 : (i : ι) → Semiring (A₂ i)] [inst_3 : (i : ι) → Algebra R (A₁ i)]
  [inst_4 : (i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i),
  (AlgEquiv.piCongrRight e).symm = AlgEquiv.piCongrRight fun i => (e i).symm

Defined in

Mathlib.Algebra.Algebra.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra