Theorems · Definition · group theory

MonoidWithZeroHom.valueGroup

{A : Type u_1} → {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : MonoidWithZero B] → (A →*₀ B) → Subgroup Bˣ

For a morphism of monoids with zero f, this is the smallest subgroup of the invertible elements in the codomain containing the range of f.

Defined in

Mathlib.Algebra.GroupWithZero.Range

Cited by

170 results in Mathlib

Foundations

Depth 67 from the axioms, rests on 818 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MonoidWithZeroMonoidWithZero