Theorems · Definition · group theory

MulEquiv.monoidHomCongrLeft

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

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

Defined in

Mathlib.Algebra.Group.Equiv.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClassCommMonoid