Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_ProjectiveWeierstrassPolynomialPrime.lean

definition module

Irreducibility of the projective Weierstrass cubic

Fix a commutative ring F and a projective Weierstrass curve V over F, i.e. data a_1,a_2,a_3,a_4,a_6 together with the homogeneous cubic V.\mathtt{polynomial} = Y^2Z + a_1XYZ + a_3YZ^2 - X^3 - a_2X^2Z - a_4XZ^2 - a_6Z^3 in three variables X = X_0, Y = X_1, Z = X_2. The module's one definition, wCubic V, is the cubic in one variable over F[Y,Z] (a two-variable polynomial ring, with X_0, X_1 there playing the roles of Y,Z) whose coefficients are, in descending order, 1, a_2Z, a_4Z^2 - a_1YZ and a_6Z^3 - Y^2Z - a_3YZ^2. Three coefficient lemmas record these entries, and finSuccEquiv_polynomial states that the image of V.\mathtt{polynomial} under the isomorphism F[X_0,X_1,X_2] \cong (F[X_0,X_1])[X] splitting off the first variable is -\,(wCubic V).toPoly.

The remaining results exploit this presentation. wCubic_toPoly_monic and, over a domain, wCubic_toPoly_natDegree give monicity and degree 3; wCubic_isEisensteinAt asserts the Eisenstein condition at the ideal generated by Z (leading coefficient outside the ideal, lower coefficients inside it, constant coefficient outside its square), whence irreducible_wCubic_toPoly and, transporting along the isomorphism, irreducible_polynomial: the Weierstrass cubic is irreducible over any domain, hence nonzero and not a unit. When F is moreover a unique factorisation domain, it is prime, the ideal it spans is prime, and the quotient F[X,Y,Z]/(V.\mathtt{polynomial}) is an integral domain. Independently of domain hypotheses, isHomogeneous_polynomial gives homogeneity of degree 3, and over a domain the total degree is 3. A final group of declarations instantiates all of this at the two rational curves \langle 0,0,1,0,0\rangle and \langle 0,0,0,1,0\rangle, including the values 2 and 1 of their cubics at (0,1,1) and the resulting distinctness of the two polynomials.

Relation to Mathlib

Built entirely on Mathlib: WeierstrassCurve.Projective and its polynomial, Mathlib's Cubic type, Polynomial.IsEisensteinAt, and the isomorphism MvPolynomial.finSuccEquiv. The only new notion is the auxiliary one-variable cubic wCubic over the coefficient ring F[Y,Z].

Where it is used

The primality of the Weierstrass cubic, and the consequent integrality of the quotient ring, are what is needed to treat F[X,Y,Z]/(V.\mathtt{polynomial}) as the homogeneous coordinate ring of a projective Weierstrass model.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd ed., 2009, Ch. III
  2. S. Lang, Algebra, Graduate Texts in Mathematics 211, Springer, 3rd ed., 2002, Ch. IV

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicGeometry_ProjectiveWeierstrassPolynomialPrime.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

open MvPolynomial

namespace ProjWeierstrassCubicPrime

section CommRing

variable {F : Type*} [CommRing F]

noncomputable def wCubic (V : WeierstrassCurve.Projective F) : Cubic (MvPolynomial (Fin 2) F) :=
  ⟨1, C V.a₂ * X 1, C V.a₄ * X 1 ^ 2 - C V.a₁ * X 0 * X 1,
    C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2⟩

theorem wCubic_toPoly_coeff_zero (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 0
      = C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2 := by
  rw [Cubic.coeff_eq_d]
  rfl

theorem wCubic_toPoly_coeff_one (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 1 = C V.a₄ * X 1 ^ 2 - C V.a₁ * X 0 * X 1 := by
  rw [Cubic.coeff_eq_c]
  rfl

theorem wCubic_toPoly_coeff_two (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 2 = C V.a₂ * X 1 := by
  rw [Cubic.coeff_eq_b]
  rfl

theorem finSuccEquiv_polynomial (V : WeierstrassCurve.Projective F) :
    finSuccEquiv F 2 V.polynomial = -(wCubic V).toPoly := by
  have h1 : (1 : Fin 3) = (0 : Fin 2).succ := rfl
  have h2 : (2 : Fin 3) = (1 : Fin 2).succ := rfl
  have hC : ∀ a : F, finSuccEquiv F 2 (C a) = Polynomial.C (C a) := fun a => by
    simp [finSuccEquiv_apply]
  rw [WeierstrassCurve.Projective.polynomial, wCubic, Cubic.toPoly]
  simp only [map_add, map_sub, map_mul, map_pow, map_one, finSuccEquiv_X_zero, h1, h2,
    finSuccEquiv_X_succ, hC]
  ring

theorem wCubic_toPoly_monic (V : WeierstrassCurve.Projective F) : (wCubic V).toPoly.Monic :=
  Cubic.monic_of_a_eq_one rfl

end CommRing

section IsDomain

variable {F : Type*} [CommRing F] [IsDomain F]

theorem wCubic_toPoly_natDegree (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.natDegree = 3 :=
  Cubic.natDegree_of_a_ne_zero one_ne_zero

theorem wCubic_isEisensteinAt (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.IsEisensteinAt (Ideal.span {(X 1 : MvPolynomial (Fin 2) F)}) := by
  refine ⟨?_, ?_, ?_⟩
  ·
    rw [(wCubic_toPoly_monic V).leadingCoeff]
    intro h
    rw [Ideal.mem_span_singleton] at h
    exact MvPolynomial.X_prime.not_unit (isUnit_of_dvd_one h)
  ·
    intro n hn
    rw [wCubic_toPoly_natDegree V] at hn
    interval_cases n
    · rw [wCubic_toPoly_coeff_zero, Ideal.mem_span_singleton]
      exact ⟨C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1, by ring⟩
    · rw [wCubic_toPoly_coeff_one, Ideal.mem_span_singleton]
      exact ⟨C V.a₄ * X 1 - C V.a₁ * X 0, by ring⟩
    · rw [wCubic_toPoly_coeff_two, Ideal.mem_span_singleton]
      exact ⟨C V.a₂, by ring⟩
  ·
    rw [wCubic_toPoly_coeff_zero, Ideal.span_singleton_pow, Ideal.mem_span_singleton]
    intro hdvd
    have he : (X 1 : MvPolynomial (Fin 2) F)
        * (C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1)
        = C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2 := by ring
    have h2 : (X 1 : MvPolynomial (Fin 2) F)
        ∣ C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1 := by
      refine (mul_dvd_mul_iff_left (MvPolynomial.X_ne_zero (1 : Fin 2))).mp ?_
      rw [show (X 1 : MvPolynomial (Fin 2) F) * X 1 = X 1 ^ 2 from (pow_two _).symm, he]
      exact hdvd
    have h3 : (X 1 : MvPolynomial (Fin 2) F) ∣ X 0 ^ 2 := by
      have h4 := dvd_sub (dvd_sub
        (dvd_mul_right (X 1 : MvPolynomial (Fin 2) F) (C V.a₆ * X 1))
        (dvd_mul_right (X 1 : MvPolynomial (Fin 2) F) (C V.a₃ * X 0))) h2
      have h5 : X 1 * (C V.a₆ * X 1) - X 1 * (C V.a₃ * X 0)
          - (C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1)
          = (X 0 ^ 2 : MvPolynomial (Fin 2) F) := by ring
      rwa [h5] at h4
    have h6 : (X 1 : MvPolynomial (Fin 2) F) ∣ X 0 :=
      MvPolynomial.X_prime.dvd_of_dvd_pow h3
    rw [MvPolynomial.X_dvd_X] at h6
    exact absurd h6 (by decide)

theorem irreducible_wCubic_toPoly (V : WeierstrassCurve.Projective F) :
    Irreducible (wCubic V).toPoly :=
  (wCubic_isEisensteinAt V).irreducible
    ((Ideal.span_singleton_prime (MvPolynomial.X_ne_zero _)).mpr MvPolynomial.X_prime)
    (wCubic_toPoly_monic V).isPrimitive
    (by rw [wCubic_toPoly_natDegree V]; norm_num)

theorem irreducible_polynomial (V : WeierstrassCurve.Projective F) :
    Irreducible V.polynomial := by
  have hneg : Irreducible (-(wCubic V).toPoly) :=
    (Associated.irreducible ⟨-1, by simp⟩ (irreducible_wCubic_toPoly V))
  have himg : Irreducible (finSuccEquiv F 2 V.polynomial) := by
    rw [finSuccEquiv_polynomial V]
    exact hneg
  exact (MulEquiv.irreducible_iff (finSuccEquiv F 2)).mp himg

theorem polynomial_ne_zero (V : WeierstrassCurve.Projective F) : V.polynomial ≠ 0 :=
  (irreducible_polynomial V).ne_zero

theorem not_isUnit_polynomial (V : WeierstrassCurve.Projective F) : ¬IsUnit V.polynomial :=
  (irreducible_polynomial V).not_isUnit

end IsDomain

section UFD

variable {F : Type*} [CommRing F] [IsDomain F] [UniqueFactorizationMonoid F]

theorem prime_polynomial (V : WeierstrassCurve.Projective F) : Prime V.polynomial :=
  UniqueFactorizationMonoid.irreducible_iff_prime.mp (irreducible_polynomial V)

theorem span_polynomial_isPrime (V : WeierstrassCurve.Projective F) :
    (Ideal.span {V.polynomial}).IsPrime :=
  (Ideal.span_singleton_prime (polynomial_ne_zero V)).mpr (prime_polynomial V)

theorem isDomain_quotient_span_polynomial (V : WeierstrassCurve.Projective F) :
    IsDomain (MvPolynomial (Fin 3) F ⧸ Ideal.span {V.polynomial}) := by
  have h : (Ideal.span {V.polynomial}).IsPrime := span_polynomial_isPrime V
  exact Ideal.Quotient.isDomain _

end UFD

section Homogeneous

variable {F : Type*} [CommRing F]

theorem isHomogeneous_polynomial (V : WeierstrassCurve.Projective F) :
    V.polynomial.IsHomogeneous 3 := by
  have hA : (X 1 ^ 2 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_X_pow (R := F) (1 : Fin 3) 2).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hB : (C V.a₁ * X 0 * X 1 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := ((isHomogeneous_C_mul_X V.a₁ (0 : Fin 3)).mul
      (isHomogeneous_X F (1 : Fin 3))).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hC : (C V.a₃ * X 1 * X 2 ^ 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X V.a₃ (1 : Fin 3)).mul (isHomogeneous_X_pow (2 : Fin 3) 2)
    norm_num at h
    exact h
  have hD : (X 0 ^ 3 : MvPolynomial (Fin 3) F).IsHomogeneous 3 :=
    isHomogeneous_X_pow (0 : Fin 3) 3
  have hE : (C V.a₂ * X 0 ^ 2 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X_pow V.a₂ (0 : Fin 3) 2).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hF : (C V.a₄ * X 0 * X 2 ^ 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X V.a₄ (0 : Fin 3)).mul (isHomogeneous_X_pow (2 : Fin 3) 2)
    norm_num at h
    exact h
  have hG : (C V.a₆ * X 2 ^ 3 : MvPolynomial (Fin 3) F).IsHomogeneous 3 :=
    isHomogeneous_C_mul_X_pow V.a₆ (2 : Fin 3) 3
  rw [WeierstrassCurve.Projective.polynomial]
  exact ((hA.add hB).add hC).sub (((hD.add hE).add hF).add hG)

theorem totalDegree_polynomial {F : Type*} [CommRing F] [IsDomain F]
    (V : WeierstrassCurve.Projective F) : V.polynomial.totalDegree = 3 :=
  (isHomogeneous_polynomial V).totalDegree (polynomial_ne_zero V)

end Homogeneous

section Gates

def gateCurveA : WeierstrassCurve ℚ := ⟨0, 0, 1, 0, 0⟩

def gateCurveB : WeierstrassCurve ℚ := ⟨0, 0, 0, 1, 0⟩

theorem gate_prime_A : Prime gateCurveA.toProjective.polynomial :=
  prime_polynomial _

theorem gate_prime_B : Prime gateCurveB.toProjective.polynomial :=
  prime_polynomial _

theorem gate_span_isPrime_A : (Ideal.span {gateCurveA.toProjective.polynomial}).IsPrime :=
  span_polynomial_isPrime _

theorem gate_isDomain_quotient_A :
    IsDomain (MvPolynomial (Fin 3) ℚ ⧸ Ideal.span {gateCurveA.toProjective.polynomial}) :=
  isDomain_quotient_span_polynomial _

theorem gate_quotient_nontrivial_A :
    Nontrivial (MvPolynomial (Fin 3) ℚ ⧸ Ideal.span {gateCurveA.toProjective.polynomial}) :=
  gate_isDomain_quotient_A.toNontrivial

theorem gate_span_ne_top_A : Ideal.span {gateCurveA.toProjective.polynomial} ≠ ⊤ :=
  gate_span_isPrime_A.ne_top

theorem gate_span_ne_bot_A : Ideal.span {gateCurveA.toProjective.polynomial} ≠ ⊥ := by
  rw [Ne, Ideal.span_singleton_eq_bot]
  exact polynomial_ne_zero _

theorem gate_eval_A :
    eval ![(0 : ℚ), 1, 1] gateCurveA.toProjective.polynomial = 2 := by
  rw [WeierstrassCurve.Projective.eval_polynomial]
  norm_num [gateCurveA, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]

theorem gate_eval_B :
    eval ![(0 : ℚ), 1, 1] gateCurveB.toProjective.polynomial = 1 := by
  rw [WeierstrassCurve.Projective.eval_polynomial]
  norm_num [gateCurveB, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]

theorem gate_polynomial_A_ne_B :
    gateCurveA.toProjective.polynomial ≠ gateCurveB.toProjective.polynomial := by
  intro h
  have hA := gate_eval_A
  rw [h, gate_eval_B] at hA
  norm_num at hA

theorem gate_isHomogeneous_A : gateCurveA.toProjective.polynomial.IsHomogeneous 3 :=
  isHomogeneous_polynomial _

theorem gate_totalDegree_A : gateCurveA.toProjective.polynomial.totalDegree = 3 :=
  totalDegree_polynomial _

end Gates

end ProjWeierstrassCubicPrime

/--
info: 'ProjWeierstrassCubicPrime.wCubic' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_zero
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_one' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_one
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_two' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_two
/--
info: 'ProjWeierstrassCubicPrime.finSuccEquiv_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.finSuccEquiv_polynomial
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_monic' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_monic
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_natDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_natDegree
/--
info: 'ProjWeierstrassCubicPrime.wCubic_isEisensteinAt' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_isEisensteinAt
/--
info: 'ProjWeierstrassCubicPrime.irreducible_wCubic_toPoly' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.irreducible_wCubic_toPoly
/--
info: 'ProjWeierstrassCubicPrime.irreducible_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.irreducible_polynomial
/--
info: 'ProjWeierstrassCubicPrime.polynomial_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.polynomial_ne_zero
/--
info: 'ProjWeierstrassCubicPrime.not_isUnit_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.not_isUnit_polynomial
/--
info: 'ProjWeierstrassCubicPrime.prime_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.prime_polynomial
/--
info: 'ProjWeierstrassCubicPrime.span_polynomial_isPrime' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.span_polynomial_isPrime
/--
info: 'ProjWeierstrassCubicPrime.isDomain_quotient_span_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.isDomain_quotient_span_polynomial
/--
info: 'ProjWeierstrassCubicPrime.isHomogeneous_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.isHomogeneous_polynomial
/--
info: 'ProjWeierstrassCubicPrime.totalDegree_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.totalDegree_polynomial
/--
info: 'ProjWeierstrassCubicPrime.gateCurveA' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gateCurveA
/--
info: 'ProjWeierstrassCubicPrime.gateCurveB' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gateCurveB
/--
info: 'ProjWeierstrassCubicPrime.gate_prime_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_prime_A
/--
info: 'ProjWeierstrassCubicPrime.gate_prime_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_prime_B
/--
info: 'ProjWeierstrassCubicPrime.gate_span_isPrime_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_isPrime_A
/--
info: 'ProjWeierstrassCubicPrime.gate_isDomain_quotient_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_isDomain_quotient_A
/--
info: 'ProjWeierstrassCubicPrime.gate_quotient_nontrivial_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_quotient_nontrivial_A
/--
info: 'ProjWeierstrassCubicPrime.gate_span_ne_top_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_ne_top_A
/--
info: 'ProjWeierstrassCubicPrime.gate_span_ne_bot_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_ne_bot_A
/--
info: 'ProjWeierstrassCubicPrime.gate_eval_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_eval_A
/--
info: 'ProjWeierstrassCubicPrime.gate_eval_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_eval_B
/--
info: 'ProjWeierstrassCubicPrime.gate_polynomial_A_ne_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_polynomial_A_ne_B
/--
info: 'ProjWeierstrassCubicPrime.gate_isHomogeneous_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_isHomogeneous_A
/--
info: 'ProjWeierstrassCubicPrime.gate_totalDegree_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_totalDegree_A

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).