finrank_eq_rank

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

URI: https://scilib.ai/kg/mathlib#NumberField.Units.finrank_eq_rank

← MathLib Explorer

English

The map logEmbeddingQuot is injective.

Русский

Отображение logEmbeddingQuot инъективно.

LaTeX

$$$\operatorname{Injective}(\logEmbeddingQuot K)$$$

Lean4

protected theorem finrank_eq_rank : finrank ℝ (logSpace K) = Units.rank K := by
  classical simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, rank]

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

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

Разделы

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

Аффилиация

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