fieldEquivOfAlgEquiv_trans — Mathlib

English

The field equivalence for a composed algebra equivalence equals the composition of the corresponding field equivalences.

Русский

Эквивалентность поля для составленного алгебраического эквивалента равна составу соответствующих эквивалентов поля.

LaTeX

$$$fieldEquivOfAlgEquiv_{FA,FB,FD}(f\,trans g) = (fieldEquivOfAlgEquiv_{FA,FB,FC} f)\,trans (fieldEquivOfAlgEquiv_{FA,FC,FD} g)$$$

Lean4

theorem fieldEquivOfAlgEquiv_trans (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) :
    fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
      (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g) :=
  by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
  simp

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