map

Mathlib.Algebra.Group.Invertible.Basic

URI: https://scilib.ai/kg/mathlib#Invertible.map

Lean4

/-- Monoid homs preserve invertibility. -/
def map {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [MulOneClass S] [FunLike F R S] [MonoidHomClass F R S]
    (f : F) (r : R) [Invertible r] : Invertible (f r)
    where
  invOf := f (⅟r)
  invOf_mul_self := by rw [← map_mul, invOf_mul_self, map_one]
  mul_invOf_self := by rw [← map_mul, mul_invOf_self, map_one]

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

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

Разделы

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

Аффилиация

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