instIsAlgebraicQuotientIdealResidueField

English

If p is prime, there is an algebraic relation of A ⧸ p over p.ResidueField, i.e., A ⧸ p is algebraic over p.ResidueField.

Русский

Если p простая, то A/ p алгебраически зависимо над p.ResidueField.

LaTeX

$$$\text{[p.IsPrime]} \Rightarrow \mathrm{Algebra.IsAlgebraic}(\mathrmHasQuotient(A,p), p.\mathrmResidueField)$$$

Lean4

instance [p.IsPrime] : Algebra.IsAlgebraic (A ⧸ p) p.ResidueField :=
  IsLocalization.isAlgebraic _ (nonZeroDivisors (A ⧸ p))

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