dual_surjective_of_injective

Mathlib.Algebra.Module.CharacterModule

URI: https://scilib.ai/kg/mathlib#CharacterModule.dual_surjective_of_injective

← MathLib Explorer

English

If f is injective, then the dual map dual f is surjective.

Русский

Если f инъективно отображает A в B, то дуальное отображение dual f сюръективно.

LaTeX

$$Injective f ⇒ Surjective (dual f)$$

Lean4

theorem dual_surjective_of_injective (f : A →ₗ[R] B) (hf : Function.Injective f) : Function.Surjective (dual f) :=
  (Module.Baer.of_divisible _).extension_property_addMonoidHom _ hf

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

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

Разделы

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

Аффилиация

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