isAlgebraic — Mathlib

English

If M is a submonoid of R and S is a localization of R at M, then S is algebraic over R.

Русский

Если M—подмножество монойда R, и S — локализация R по M, то S алгебраична над R.

LaTeX

$$$ [Nontrivial R] (M : Submonoid R) [IsLocalization M S] : Algebra.IsAlgebraic R S $$$

Lean4

theorem isAlgebraic [Nontrivial R] (M : Submonoid R) [IsLocalization M S] : Algebra.IsAlgebraic R S where
  isAlgebraic
    x := by
    obtain rfl | hx := eq_or_ne x 0
    · exact isAlgebraic_zero
    have ⟨⟨r, m⟩, h⟩ := surj M x
    refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using h⟩
    rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h

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