instGroupWithZeroSubtypeMemSubmonoidMrange

Mathlib.Algebra.GroupWithZero.Submonoid.Instances

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

Lean4

instance [GroupWithZero G] [GroupWithZero H] (f : G →*₀ H) : GroupWithZero (MonoidHom.mrange f)
    where
  inv := fun x ↦
    ⟨x⁻¹, by
      obtain ⟨y, hy⟩ := x.prop
      use y⁻¹
      simp [← hy]⟩
  exists_pair_ne := ⟨⟨f 0, 0, rfl⟩, ⟨f 1, by simp [-map_one]⟩, by simp⟩
  inv_zero := Subtype.ext inv_zero
  mul_inv_cancel := by
    rintro ⟨a, ha⟩ h
    simp only [ne_eq, Subtype.ext_iff] at h
    simpa using mul_inv_cancel₀ h

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

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

Разделы

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

Аффилиация

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