isLocalHom_equiv

Mathlib.Algebra.Group.Units.Equiv

URI: https://scilib.ai/kg/mathlib#isLocalHom_equiv

English

Let x be a unit in a division monoid G, and f,g be homomorphisms. If f(x) = g(x), then f(x⁻¹) = g(x⁻¹).

Русский

Пусть x — элемент-единица в DivisionMonoid G, и f,g — гомоморфизмы. Если f(x) = g(x), то f(x⁻¹) = g(x⁻¹).

LaTeX

$$$\\text{IsUnit}(x) \\Rightarrow f(x)=g(x) \\Rightarrow f(x^{-1})=g(x^{-1})$$$

Lean4

@[instance]
theorem isLocalHom_equiv : IsLocalHom f where map_nonunit := by simp

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

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

Разделы

Аффилиация

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