trdeg_eq

Mathlib.RingTheory.AlgebraicIndependent.Basic

URI: https://scilib.ai/kg/mathlib#AlgEquiv.trdeg_eq

← MathLib Explorer

English

If e: A ≃ₐ[R] A' is an algebra equivalence, then trdeg R A = trdeg R A'.

Русский

Если e: A ≃ₐ[R] A' является алгебраическим эквивалентом, то trdeg R A = trdeg R A'.

LaTeX

$$$\trdeg R A = \trdeg R A'.$$$

Lean4

theorem trdeg_eq {A' : Type v} [CommRing A'] [Algebra R A'] (e : A ≃ₐ[R] A') : trdeg R A = trdeg R A' := by
  rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]

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

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

Разделы

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

Аффилиация

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