isFractionRing_iff_of_base_ringEquiv

English

Fraction ring property is preserved under base ring isomorphisms.

Русский

Свойство дробной локализации сохраняется при изоморфизма базовых колец.

LaTeX

$$$IsFractionRing R S \;\Leftrightarrow\; IsFractionRing P S$ under a ring equivalence $h : R \to P$$$

Lean4

theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) :
    IsFractionRing R S ↔ @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra :=
  by
  delta IsFractionRing
  convert isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h
  exact (MulEquivClass.map_nonZeroDivisors h).symm

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