ker_algebraMap_eq_bot

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#FaithfulSMul.ker_algebraMap_eq_bot

← MathLib Explorer

English

If the action is faithful, the kernel of the algebra map is {0}.

Русский

Если действие верно фиктивно, ядро алгебраического отображения равно нулю.

LaTeX

$$$$ \\ker(\\text{algebraMap } R A) = 0. $$$$

Lean4

@[simp]
theorem ker_algebraMap_eq_bot (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] :
    RingHom.ker (algebraMap R A) = ⊥ := by ext; simp

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

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

Разделы

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

Аффилиация

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