ofBijective

Mathlib.Algebra.Star.StarRingHom

URI: https://scilib.ai/kg/mathlib#StarRingEquiv.ofBijective

Lean4

/-- Promote a bijective star ring homomorphism to a star ring equivalence. -/
noncomputable def ofBijective (f : F) (hf : Function.Bijective f) : A ≃⋆+* B :=
  {
    RingEquiv.ofBijective f (hf : Function.Bijective
          (f : A → B)) with
    toFun := f
    map_star' := map_star f }

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

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

Разделы

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

Аффилиация

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