Theorems · Theorem · ring theory

SkewMonoidAlgebra.domCongr_symm

∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x),
  (SkewMonoidAlgebra.domCongrAlg k A he).symm = SkewMonoidAlgebra.domCongrAlg k A ⋯

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidMonoidSemiringCommSemiringAlgebraMulSemiringActionMulSemiringActionSMulCommClassSMulCommClass