theorem irreducible_dvd_or_coprime {R : Type u_1} [CommRing R] [IsBezout R] {Q : R} (hQ : Irreducible Q) (P : R) : Q ∣ P ∨ IsCoprime Q P

In a Bezout domain, an irreducible element either divides any given element or is coprime to it.

theorem irreducible_dvd_of_not_coprime {R : Type u_1} [CommRing R] [IsBezout R] {Q P : R} (hQ : Irreducible Q) (h : ¬IsCoprime Q P) : Q ∣ P

If an irreducible element is not coprime to P in a Bezout domain, then it divides P.

theorem irreducible_dvd_iff_not_coprime {R : Type u_1} [CommRing R] [IsBezout R] {Q P : R} (hQ : Irreducible Q) : Q ∣ P ↔ ¬IsCoprime Q P

In a Bezout domain, divisibility by an irreducible is equivalent to non-coprimality.

theorem irreducible_dvd_mul {R : Type u_1} [CommRing R] [IsBezout R] {Q a b : R} (hQ : Irreducible Q) (h : Q ∣ a * b) : Q ∣ a ∨ Q ∣ b

In a Bezout domain, an irreducible dividing a product divides one of the factors.

theorem natDegree_mul_three_linear_le {R : Type u_1} [CommRing R] {L₁ L₃ L₅ : Polynomial R} (h₁ : L₁.natDegree ≤ 1) (h₃ : L₃.natDegree ≤ 1) (h₅ : L₅.natDegree ≤ 1) : (L₁ * L₃ * L₅).natDegree ≤ 3

Degree bound: a triple product of polynomials of degree ≤ 1 has degree ≤ 3.

theorem pascal_theorem {k : Type u_1} [Field k] (Q : Polynomial k) (hQ : Irreducible Q) (_hd : Q.natDegree = 2) (F G : Polynomial k) (_hF : F.natDegree ≤ 3) (_hG : G.natDegree ≤ 3) (h_not_coprime : ¬IsCoprime Q (F - G)) : Q ∣ F - G

Pascal's theorem (Theorem 5.3, Lecture 5), Bezout step: if an irreducible conic Q shares a point with two cubics F and G (so Q is not coprime to F - G), then Q divides F - G.

theorem pascal_collinearity {k : Type u_1} [Field k] {Q F G : Polynomial k} (hQm : Q.Monic) (hQd : Q.natDegree = 2) (hF : F.natDegree ≤ 3) (hG : G.natDegree ≤ 3) (_hdvd : Q ∣ F - G) : ((F - G) /ₘ Q).natDegree ≤ 1

After dividing F - G by the conic Q, the quotient is a polynomial of degree ≤ 1: the Pascal line on which the three intersection points lie.

theorem pascal_full {k : Type u_1} [Field k] (Q : Polynomial k) (hQ : Irreducible Q) (hQm : Q.Monic) (hQd : Q.natDegree = 2) {L₁ L₂ L₃ L₄ L₅ L₆ : Polynomial k} (hL₁ : L₁.natDegree ≤ 1) (hL₂ : L₂.natDegree ≤ 1) (hL₃ : L₃.natDegree ≤ 1) (hL₄ : L₄.natDegree ≤ 1) (hL₅ : L₅.natDegree ≤ 1) (hL₆ : L₆.natDegree ≤ 1) (h_not_coprime : ¬IsCoprime Q (L₁ * L₃ * L₅ - L₂ * L₄ * L₆)) : Q ∣ L₁ * L₃ * L₅ - L₂ * L₄ * L₆ ∧ ((L₁ * L₃ * L₅ - L₂ * L₄ * L₆) /ₘ Q).natDegree ≤ 1

Full Pascal statement for hexagons: with six lines L_1,...,L_6 forming an inscribed hexagon in the conic Q, the difference of the two cubic products is divisible by Q and the resulting quotient is the Pascal line.

theorem krullDimLE_one_of_ringKrullDim_eq_one {A : Type u_1} [CommRing A] (hdim : ringKrullDim A = 1) : Ring.KrullDimLE 1 A

If a ring has Krull dimension exactly 1, it satisfies KrullDimLE 1.

theorem dim_one_prime_is_maximal {A : Type u_1} [CommRing A] [IsDomain A] (hdim : ringKrullDim A = 1) {p : Ideal A} (hp : p.IsPrime) (hne : p ≠ ⊥) : p.IsMaximal

In a 1-dimensional domain, every nonzero prime ideal is maximal.

theorem dim_one_proper_closed_finite {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (hdim : ringKrullDim A = 1) (I : Ideal A) (hI : I ≠ ⊥) (_hI' : I ≠ ⊤) : {p : Ideal A | p.IsPrime ∧ I ≤ p}.Finite

A proper nonzero closed subset of a Noetherian 1-dimensional affine curve is finite (a finite set of points).

noncomputable def cofiniteEquiv (X : Type u_1) (Y : Type u_2) (e : X ≃ Y) : CofiniteTopology X ≃ CofiniteTopology Y

Equivalence between cofinite topologies induced by an underlying type equivalence.

theorem cofinite_continuous_of_equiv (X : Type u_1) (Y : Type u_2) (e : X ≃ Y) : Continuous ⇑(cofiniteEquiv X Y e)

The cofinite equivalence map is continuous in the cofinite topologies.

noncomputable def cofiniteHomeomorph (X : Type u_1) (Y : Type u_2) (e : X ≃ Y) : CofiniteTopology X ≃ₜ CofiniteTopology Y

A type equivalence promotes to a homeomorphism between cofinite topologies.

theorem irreducible_curves_homeomorphic_of_algClosed (k : Type u_1) [Field k] [IsAlgClosed k] {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [IsNoetherianRing A] [IsNoetherianRing B] [Algebra k A] [Algebra k B] (hdimA : ringKrullDim A = 1) (hdimB : ringKrullDim B = 1) : Nonempty (PrimeSpectrum A ≃ₜ PrimeSpectrum B)

Any two irreducible affine curves over an algebraically closed field are homeomorphic in the Zariski topology, since both are countably infinite cofinite topological spaces.