FaithfulSMulLeft

Mathlib.Algebra.Group.Action.Sum

URI: https://scilib.ai/kg/mathlib#Sum.FaithfulSMulLeft

← MathLib Explorer

English

If M acts faithfully on α, then it acts faithfully on α ⊕ β.

Русский

Если M верно действует на α, то действие на α ⊕ β тоже верно.

LaTeX

$$$[FaithfulSMul M α] \Rightarrow FaithfulSMul M (α \oplus β).$$$

Lean4

@[to_additive]
instance FaithfulSMulLeft [FaithfulSMul M α] : FaithfulSMul M (α ⊕ β) :=
  ⟨fun h => eq_of_smul_eq_smul fun a : α => by injection h (inl a)⟩

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

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

Разделы

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

Аффилиация

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