fieldEquivOfAlgEquiv_refl — Mathlib

English

The field isomorphism associated to the identity algebra equivalence is the identity on the fraction fields.

Русский

Изоморфизм поля, связанный с тождественным алгебраическим эквивалентом, является тождественным на дробных полях.

LaTeX

$$$IsFractionRing.fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl) = AlgEquiv.refl$$$

Lean4

@[simp]
theorem fieldEquivOfAlgEquiv_refl : fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl :=
  by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
  simp

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