relrank_map_map

Mathlib.FieldTheory.Relrank

URI: https://scilib.ai/kg/mathlib#Subfield.relrank_map_map

← MathLib Explorer

English

For a field homomorphism f, relrank((A.map f),(B.map f)) = relrank(A,B).

Русский

При отображении f ранг A над B сохраняется: relrank(A.map f, B.map f) = relrank(A,B).

LaTeX

$$$ \operatorname{relrank}(A.map f, B.map f) = \operatorname{relrank}(A,B)$$$

Lean4

theorem relrank_map_map {L : Type v} [Field L] (f : E →+* L) : relrank (A.map f) (B.map f) = relrank A B := by
  simpa only [lift_id] using lift_relrank_map_map A B f

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

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

Разделы

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

Аффилиация

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