Theorems · Definition · ring theory

SkewMonoidAlgebra.equivMapDomain

{k : Type u_1} →
  {G : Type u_2} → {H : Type u_3} → [inst : AddCommMonoid k] → G ≃ H → SkewMonoidAlgebra k G → SkewMonoidAlgebra k H

Given f : G ≃ H, we can map l : SkewMonoidAlgebra k G to equivMapDomain f l : SkewMonoidAlgebra k H (computably) by mapping the support forwards and the function backwards.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

7 results in Mathlib

Foundations

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

Assumes

AddCommMonoid