instFaithfulSMul

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#Module.Invertible.instFaithfulSMul

English

If N is an invertible R-module and f: M → N is surjective, then f is bijective.

Русский

Если N — обратимый R-модуль и f: M → N сюрьективно, то f является биективным.

LaTeX

$$$[Module.Invertible R N] \land \operatorname{Surjective}(f) \Rightarrow \operatorname{Bijective}(f)$$$

Lean4

instance : FaithfulSMul R M where eq_of_smul_eq_smul {_ _} h := (toModuleEnd_bijective R M).injective <| LinearMap.ext h

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

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

Разделы

Аффилиация

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