int

Mathlib.Algebra.Module.CharacterModule

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

Lean4

/-- `ℤ⋆`, the character module of `ℤ` in the unit rational circle.
-/
protected abbrev int : Type :=
  CharacterModule ℤ

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

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

Разделы

Аффилиация

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