natCard_eq

Mathlib.LinearAlgebra.FreeModule.ModN

URI: https://scilib.ai/kg/mathlib#ModN.natCard_eq

← MathLib Explorer

English

The Nat-card of ModN G n equals n raised to the rank of G over ℤ.

Русский

Кардинал Нат равен $n^{\operatorname{rank}_{\mathbb{Z}} G}$.

LaTeX

$$Nat.card (ModN G n) = n ^ Module.finrank ℤ G$$

Lean4

@[simp]
theorem natCard_eq : Nat.card (ModN G n) = n ^ Module.finrank ℤ G := by
  simp [Nat.card_congr (basis <| Module.Free.chooseBasis ℤ G).repr.toEquiv, Nat.card_eq_fintype_card,
    Module.finrank_eq_card_chooseBasisIndex]

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

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

Разделы

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

Аффилиация

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