Theorems · Definition · group theory

MonoidWithZeroHom.inl

(G₀ : Type u_1) →
  (H₀ : Type u_2) →
    [inst : GroupWithZero G₀] →
      [inst_1 : GroupWithZero H₀] → [DecidablePred fun x => x = 0] → G₀ →*₀ WithZero (G₀ˣ × H₀ˣ)

Given groups with zero G₀, H₀, the natural inclusion ordered homomorphism from G₀ to WithZero (G₀ˣ × H₀ˣ), which is the group with zero that can be identified as their product.

Defined in

Mathlib.Algebra.GroupWithZero.ProdHom

Cited by

13 results in Mathlib

Foundations

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

Assumes

GroupWithZeroGroupWithZeroDecidablePred