toMonoidWithZeroHom_inj

Mathlib.Algebra.GroupWithZero.Equiv

URI: https://scilib.ai/kg/mathlib#MulEquiv.toMonoidWithZeroHom_inj

← MathLib Explorer

English

The equivalence to MonoidWithZeroHom is injective in the extensional sense.

Русский

Эквивалентность к MonoidWithZeroHom инъективна по отношению к ext_iff.

LaTeX

$$$f.toMonoidWithZeroHom = g.toMonoidWithZeroHom \\Rightarrow f = g$$$

Lean4

@[simp]
theorem toMonoidWithZeroHom_inj {f g : G ≃* H} : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g := by
  simp [MonoidWithZeroHom.ext_iff, MulEquiv.ext_iff]

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

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

Разделы

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

Аффилиация

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