Theorems · Theorem · group theory

MonoidWithZeroHom.fst_comp_inl

∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0],
  (MonoidWithZeroHom.fst G₀ H₀).comp (MonoidWithZeroHom.inl G₀ H₀) = MonoidWithZeroHom.id G₀

Defined in

Mathlib.Algebra.GroupWithZero.ProdHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupWithZeroGroupWithZeroDecidablePred