valueMonoid

Mathlib.Algebra.GroupWithZero.Range

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.valueMonoid

Lean4

/-- 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`. -/
def valueMonoid : Submonoid Bˣ where
  carrier := (↑) ⁻¹' (range f)
  mul_mem' hb
    hb' := by
    obtain ⟨y, hy⟩ := hb
    obtain ⟨y', hy'⟩ := hb'
    use y * y'
    rw [map_mul, hy, hy', Units.val_mul]
  one_mem' := ⟨1, by simp⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru