Theorems · Definition · group theory

MonoidWithZeroHom.fst

(G₀ : Type u_1) →
  (H₀ : Type u_2) → [inst : GroupWithZero G₀] → [inst_1 : GroupWithZero H₀] → WithZero (G₀ˣ × H₀ˣ) →*₀ G₀

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

Defined in

Mathlib.Algebra.GroupWithZero.ProdHom

Cited by

10 results in Mathlib

Foundations

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

Assumes

GroupWithZeroGroupWithZero