inv

Mathlib.MeasureTheory.Group.MeasurableEquiv

URI: https://scilib.ai/kg/mathlib#MeasurableEquiv.inv

Lean4

/-- Inversion as a measurable automorphism of a group or group with zero. -/
@[to_additive (attr := simps! -fullyApplied toEquiv apply) /--
    Negation as a measurable automorphism of an additive group. -/
    ]
def inv (G) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : G ≃ᵐ G
    where
  toEquiv := Equiv.inv G
  measurable_toFun := measurable_inv
  measurable_invFun := measurable_inv

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

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

Разделы

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

Аффилиация

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