Theorems · Theorem · group theory

AddMonoid.Coprod.clift_apply_inr

∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y)))
  (x : N), (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inr x) = f (FreeAddMonoid.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

AddZeroClassAddZeroClassAddZeroClass