Theorems · Definition · group theory

MulEquiv.monoidHomCongrLeftEquiv

{M₁ : Type u_5} →
  {M₂ : Type u_6} →
    {N : Type u_8} →
      [inst : MulOneClass M₁] → [inst_1 : MulOneClass M₂] → [inst_2 : Monoid N] → M₁ ≃* M₂ → (M₁ →* N) ≃ (M₂ →* N)

The equivalence (M₁ →* N) ≃ (M₂ →* N) obtained by postcomposition with a multiplicative equivalence e : M₁ ≃* M₂.

Defined in

Mathlib.Algebra.Group.Equiv.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClassMonoid