Theorems · Theorem · group theory

MonoidWithZeroHom.commute_inl_inr

∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : DecidablePred fun x => x = 0] (m : G₀) (n : H₀),
  Commute ((MonoidWithZeroHom.inl G₀ H₀) m) ((MonoidWithZeroHom.inr G₀ H₀) n)

Defined in

Mathlib.Algebra.GroupWithZero.ProdHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupWithZeroGroupWithZeroDecidablePredDecidablePred