Theorems · Theorem · group theory

Monoid.Coprod.clift_apply_inr

∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y)))
  (x : N), (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inr x) = f (FreeMonoid.of (Sum.inr x))

Defined in

Mathlib.GroupTheory.Coprod.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClassMulOneClass