Theorems · Definition · group theory

MonoidWithZeroHom.valueMonoid

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

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

Defined in

Mathlib.Algebra.GroupWithZero.Range

Cited by

10 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

MonoidWithZeroMonoidWithZero