eq_zero_of_character_apply

Mathlib.Algebra.Module.CharacterModule

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

← MathLib Explorer

English

If a is determined to be zero by all characters, then a = 0.

Русский

Если все характеры дают ноль при приложении к a, то a = 0.

LaTeX

$$Eq_zero_of_character_apply$$

Lean4

theorem eq_zero_of_character_apply {a : A} (h : ∀ c : CharacterModule A, c a = 0) : a = 0 := by contrapose! h;
  exact exists_character_apply_ne_zero_of_ne_zero h

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

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

Разделы

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

Аффилиация

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