ext

Mathlib.Algebra.Module.CharacterModule

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

English

If two characters c and c' in CharacterModule A agree on all elements of A, then c = c'.

Русский

Если две характеристические отображения c и c' в CharacterModule A совпадают на всех элементах A, то c = c'.

LaTeX

$$$$ \\forall x \\in A,\\ c(x) = c'(x) \\Rightarrow c = c'. $$$$

Lean4

@[ext]
theorem ext {c c' : CharacterModule A} (h : ∀ x, c x = c' x) : c = c' :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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