ofPrimeAlgebra — Mathlib

English

There is an algebra structure of the coarsened subring over the original subring via localization.

Русский

Существует структура алгебры для упрощённого подкольца над исходным через локализацию.

LaTeX

$$Algebra A (A.ofPrime P)$$

Lean4

instance ofPrimeAlgebra (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] : Algebra A (A.ofPrime P) :=
  Subalgebra.algebra (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors)

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