API checks for the quotient P̂/I

The quotient P̂/I satisfies two conclusions of different strength: the ideal I is prime, equivalently P̂/I is a domain, and P̂/I is geometrically integral over K.

Geometric integrality is strictly stronger than integrality over K: tensoring with every field extension must give a domain, with no finiteness or separability hypothesis.

The separate nontriviality statement matters because a quotient by the whole ring would satisfy the no-zero-divisors condition vacuously, while IsDomain also requires 0 ≠ 1.

theorem Tests.coefficientIdeal_ne_top (K : Type v) [Field K] : Berarducci.principalFibreIdeal K ≠ ⊤

The ideal I = I_{≥1} is proper, so the quotient P̂/I is nontrivial, over every field.

theorem Tests.coefficientQuotient_isDomain (K : Type v) [Field K] [CharZero K] : IsDomain (Berarducci.PrincipalFibre K)

The quotient P̂/I is a domain.

theorem Tests.coefficientQuotient_isDomain_tensor (K : Type v) [Field K] [CharZero K] (L : Type (max 1 v)) [Field L] [Algebra K L] : IsDomain (TensorProduct K (Berarducci.PrincipalFibre K) L)

Tensoring P̂/I with an arbitrary field extension gives a domain.

theorem Tests.coefficientQuotient_isGeometricallyIntegral (K : Type v) [Field K] [CharZero K] : Algebra.IsGeometricallyIntegral K (Berarducci.PrincipalFibre K)

The quotient P̂/I is geometrically integral over K.