Discriminants of number fields

TheoremAbsolute norm of the discriminant ideal of a number field#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and discriminant \(d_K\). The absolute norm of the discriminant ideal of \(\mathcal{O}_K\) over \(\mathbb{Z}\) equals \(|d_K|\).

theorem absNorm_discriminantIdeal (K : Type*) [Field K] [NumberField K] :
    Ideal.absNorm (discriminantIdeal ℤ (NumberField.RingOfIntegers K)) =
      (NumberField.discr K).natAbs

Uses 2

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesThe discriminant ideal is the norm of the different

TheoremComparison of the Minkowski and exponential discriminant bounds#✓fully proved

Let \(n\) and \(s\) be natural numbers with \(n \ne 0\) and \(2s \le n\), and let \(e\) be Euler's number. Then

\[\frac{1}{e^2 n} \left(\frac{\pi e^2}{4}\right)^n < \left(\frac{n^n}{n!}\right)^2 \left(\frac{\pi}{4}\right)^{2s}.\]

theorem pow_div_factorial_sq_mul_pi_div_four_pow_gt (n s : ℕ) (hn : n ≠ 0)
    (hs : 2 * s ≤ n) :
    (1 / (Real.exp 1 ^ 2 * n)) * ((Real.pi * Real.exp 1 ^ 2) / 4) ^ n
      < ((n : ℝ) ^ n / (Nat.factorial n : ℝ)) ^ 2 *
          (Real.pi / 4) ^ (2 * s)

Sources

• ATLAS NumberTheoryI Corollary 14.26 (second inequality), with \(n\) the degree of a number field and \(s\) its number of complex places.

Used by 1

Used byExponential lower bound for the discriminant

TheoremMinkowski's lower bound for the discriminant#✓fully proved

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) with \(s\) complex places and discriminant \(d_K\). Then

\[|d_K| \ge \left(\frac{n^n}{n!}\right)^2 \left(\frac{\pi}{4}\right)^{2s}.\]

theorem middle_term_le_abs_discr (K : Type*) [Field K] [NumberField K] :
    (((Module.finrank ℚ K : ℝ) ^ (Module.finrank ℚ K) /
      (Nat.factorial (Module.finrank ℚ K) : ℝ)) ^ 2 *
      (Real.pi / 4) ^ (2 * nrComplexPlaces K)) ≤ (↑|discr K| : ℝ)

Sources

• ATLAS NumberTheoryI Corollary 14.26 (first inequality); this is Mathlib's NumberField.abs_discr_ge', restated in the form used by the book.

Used by 1

Used byExponential lower bound for the discriminant

TheoremExponential lower bound for the discriminant#✓fully proved

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) and discriminant \(d_K\), and let \(e\) be Euler's number. Then

\[|d_K| > \frac{1}{e^2 n} \left(\frac{\pi e^2}{4}\right)^n,\]

so the absolute discriminant grows at least exponentially in the degree.

theorem abs_discr_gt_exp_term (K : Type*) [Field K] [NumberField K] :
    (1 / (Real.exp 1 ^ 2 * Module.finrank ℚ K)) *
      ((Real.pi * Real.exp 1 ^ 2) / 4) ^ (Module.finrank ℚ K) <
        (↑|discr K| : ℝ)

Sources

• ATLAS NumberTheoryI Corollary 14.26 (second inequality).

Uses 2

Proof usesMinkowski's lower bound for the discriminant · Comparison of the Minkowski and exponential discriminant bounds

DefinitionDiscriminants of tuples from a submodule#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), this is the set of all discriminants \(\operatorname{disc}_{L/K}(b_1, \dots, b_n) = \det(\operatorname{Tr}_{L/K}(b_i b_j))\) in \(K\) of \(n\)-tuples \((b_1, \dots, b_n)\) of elements of \(M\).

def latticeDiscriminantSet [FiniteDimensional K L] [_hAKL : IsScalarTower A K L]
    (M : Submodule A L) : Set K :=
  {d | ∃ b : Fin (Module.finrank K L) → L, (∀ i, b i ∈ M) ∧ d = Algebra.discr K b}

Used by 6

Used byDiscriminants of tuples from \(B\) lie in the extension discriminant · Localization of the extension discriminant · Discriminant of a lattice · The discriminant of a lattice spanned by a basis · The discriminant of a lattice inside a basis lattice · The discriminant of a lattice containing a basis is nonzero

DefinitionDiscriminant of a lattice#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). The discriminant \(D(M)\) of an \(A\)-submodule \(M\) of \(L\) is the \(A\)-submodule of \(K\) generated by the discriminants \(\operatorname{disc}_{L/K}(b_1, \dots, b_n) = \det(\operatorname{Tr}_{L/K}(b_i b_j))\) of all \(n\)-tuples \((b_1, \dots, b_n)\) of elements of \(M\).

def latticeDiscriminant [_hAKL : IsScalarTower A K L]
    (M : Submodule A L) : Submodule A K :=
  Submodule.span A (latticeDiscriminantSet A K M)

Uses 1 · Used by 11

Statement usesDiscriminants of tuples from a submodule

Used byDiscriminants of tuples from \(B\) lie in the extension discriminant · Extension discriminant · The extension discriminant is a lattice discriminant · Localization of the extension discriminant · Equal discriminants force equal lattices · Equal discriminants force equal lattices (fraction field version) · The discriminant of a lattice spanned by a basis · The discriminant of a lattice inside a basis lattice is fractional · The discriminant of a sandwiched lattice is a nonzero fractional ideal · The discriminant of a lattice inside a basis lattice · The discriminant of a lattice containing a basis is nonzero

TheoremThe discriminant of a lattice inside a basis lattice#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). If \(b_1, \dots, b_n\) is a \(K\)-basis of \(L\) and \(M\) is contained in the \(A\)-span of \(b_1, \dots, b_n\), then \(D(M) \subseteq A \cdot \operatorname{disc}_{L/K}(b_1, \dots, b_n)\).

theorem latticeDiscriminant_le_span_singleton [_hAKL : IsScalarTower A K L]
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (M : Submodule A L)
    (hM : M ≤ Submodule.span A (Set.range (bK : Fin _ → L))) :
    latticeDiscriminant A K M ≤
      Submodule.span A {Algebra.discr K (bK : Fin _ → L)}

Uses 2 · Used by 2

Statement usesDiscriminant of a lattice

Proof usesDiscriminants of tuples from a submodule

Used byThe discriminant of a lattice spanned by a basis · The discriminant of a lattice inside a basis lattice is fractional

TheoremThe discriminant of a lattice inside a basis lattice is fractional#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). Assume \(K\) is the fraction field of \(A\). If \(M\) is contained in the \(A\)-span of a \(K\)-basis \(b_1, \dots, b_n\) of \(L\), then \(D(M)\) is a fractional ideal: there is a non-zero-divisor \(a \in A\) such that \(a x\) lies in the image of \(A\) in \(K\) for every \(x \in D(M)\).

theorem latticeDiscriminant_isFractional [IsFractionRing A K]
    [_hAKL : IsScalarTower A K L]
    (M : Submodule A L)
    (bN : Module.Basis (Fin (Module.finrank K L)) K L)
    (hMN : M ≤ Submodule.span A (Set.range (bN : Fin _ → L))) :
    IsFractional (nonZeroDivisors A) (latticeDiscriminant A K M)

Uses 2 · Used by 1

Statement usesDiscriminant of a lattice

Proof usesThe discriminant of a lattice inside a basis lattice

Used byThe discriminant of a sandwiched lattice is a nonzero fractional ideal

TheoremThe discriminant of a lattice containing a basis is nonzero#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). Assume \(L/K\) is separable. If \(M\) contains a \(K\)-basis \(b_1, \dots, b_n\) of \(L\), then \(D(M) \neq 0\).

theorem latticeDiscriminant_ne_bot_of_basis [_hAKL : IsScalarTower A K L]
    [Algebra.IsSeparable K L]
    (M : Submodule A L)
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (hKM : Set.range (bK : Fin _ → L) ⊆ M) :
    latticeDiscriminant A K M ≠ ⊥

Uses 2 · Used by 1

Statement usesDiscriminant of a lattice

Proof usesDiscriminants of tuples from a submodule

Used byThe discriminant of a sandwiched lattice is a nonzero fractional ideal

TheoremThe discriminant of a sandwiched lattice is a nonzero fractional ideal#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). Assume \(K\) is the fraction field of \(A\) and \(L/K\) is separable. If \(M\) contains a \(K\)-basis \(b_1, \dots, b_n\) of \(L\) and is contained in the \(A\)-span of a \(K\)-basis \(c_1, \dots, c_n\) of \(L\), then \(D(M)\) is a fractional ideal (there is a non-zero-divisor \(a \in A\) such that \(a x\) lies in the image of \(A\) in \(K\) for every \(x \in D(M)\)) and \(D(M) \neq 0\).

theorem latticeDiscriminant_isFractional_and_ne_bot [IsFractionRing A K]
    [_hAKL : IsScalarTower A K L] [Algebra.IsSeparable K L]
    (M : Submodule A L)
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (hKM : Set.range (bK : Fin _ → L) ⊆ M)
    (bN : Module.Basis (Fin (Module.finrank K L)) K L)
    (hMN : M ≤ Submodule.span A (Set.range (bN : Fin _ → L))) :
    IsFractional (nonZeroDivisors A) (latticeDiscriminant A K M) ∧
      latticeDiscriminant A K M ≠ ⊥

Uses 3

Statement usesDiscriminant of a lattice

Proof usesThe discriminant of a lattice inside a basis lattice is fractional · The discriminant of a lattice containing a basis is nonzero

TheoremThe discriminant of a lattice spanned by a basis#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). If \(b_1, \dots, b_n\) is a \(K\)-basis of \(L\), every \(b_i\) lies in \(M\) and \(M\) is contained in the \(A\)-span of \(b_1, \dots, b_n\), then \(D(M) = A \cdot \operatorname{disc}_{L/K}(b_1, \dots, b_n)\).

theorem latticeDiscriminant_eq_span_singleton [_hAKL : IsScalarTower A K L]
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (M : Submodule A L)
    (hM_le : M ≤ Submodule.span A (Set.range (bK : Fin _ → L)))
    (hM_ge : Set.range (bK : Fin _ → L) ⊆ M) :
    latticeDiscriminant A K M =
      Submodule.span A {Algebra.discr K (bK : Fin _ → L)}

Uses 3 · Used by 1

Statement usesDiscriminant of a lattice

Proof usesDiscriminants of tuples from a submodule · The discriminant of a lattice inside a basis lattice

Used byEqual discriminants force equal lattices

TheoremEqual discriminants force equal lattices#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). Assume \(L/K\) is separable and the map \(A \to K\) is injective. Let \(M' \subseteq M\) be \(A\)-submodules of \(L\). Suppose that \(b_1, \dots, b_n\) is a \(K\)-basis of \(L\) with every \(b_i\) in \(M\) and \(M\) contained in the \(A\)-span of \(b_1, \dots, b_n\), and that \(b'_1, \dots, b'_n\) is a \(K\)-basis of \(L\) with every \(b'_i\) in \(M'\) and \(M'\) contained in the \(A\)-span of \(b'_1, \dots, b'_n\). If \(D(M') = D(M)\), then \(M' = M\).

theorem latticeDiscriminant_eq_imp_eq [_hAKL : IsScalarTower A K L]
    [Algebra.IsSeparable K L]
    (hAK : Function.Injective (algebraMap A K))
    (M M' : Submodule A L) (hle : M' ≤ M)
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (hM_le : M ≤ Submodule.span A (Set.range (bK : Fin _ → L)))
    (hM_ge : Set.range (bK : Fin _ → L) ⊆ M)
    (bK' : Module.Basis (Fin (Module.finrank K L)) K L)
    (hM'_le : M' ≤ Submodule.span A (Set.range (bK' : Fin _ → L)))
    (hM'_ge : Set.range (bK' : Fin _ → L) ⊆ M')
    (hD : latticeDiscriminant A K M' = latticeDiscriminant A K M) :
    M' = M

Sources

• Sutherland, MIT 18.785 Number Theory I (Fall 2021), Lecture 12, Lemma 12.10.

Uses 2 · Used by 1

Statement usesDiscriminant of a lattice

Proof usesThe discriminant of a lattice spanned by a basis

Used byEqual discriminants force equal lattices (fraction field version)

TheoremEqual discriminants force equal lattices (fraction field version)#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a finite extension of fields, with \(A\)-algebra structures on \(K\) and \(L\) forming a scalar tower \(A \to K \to L\), and let \(n = [L : K]\). For an \(A\)-submodule \(M\) of \(L\), let \(D(M)\) be its discriminant, the \(A\)-submodule of \(K\) generated by the discriminants over \(K\) of all \(n\)-tuples of elements of \(M\). Assume \(K\) is the fraction field of \(A\) and \(L/K\) is separable. Let \(M' \subseteq M\) be \(A\)-submodules of \(L\). Suppose that \(b_1, \dots, b_n\) is a \(K\)-basis of \(L\) with every \(b_i\) in \(M\) and \(M\) contained in the \(A\)-span of \(b_1, \dots, b_n\), and that \(b'_1, \dots, b'_n\) is a \(K\)-basis of \(L\) with every \(b'_i\) in \(M'\) and \(M'\) contained in the \(A\)-span of \(b'_1, \dots, b'_n\). If \(D(M') = D(M)\), then \(M' = M\).

theorem latticeDiscriminant_eq_imp_eq_of_isFractionRing [IsFractionRing A K]
    [_hAKL : IsScalarTower A K L] [Algebra.IsSeparable K L]
    (M M' : Submodule A L) (hle : M' ≤ M)
    (bK : Module.Basis (Fin (Module.finrank K L)) K L)
    (hM_le : M ≤ Submodule.span A (Set.range (bK : Fin _ → L)))
    (hM_ge : Set.range (bK : Fin _ → L) ⊆ M)
    (bK' : Module.Basis (Fin (Module.finrank K L)) K L)
    (hM'_le : M' ≤ Submodule.span A (Set.range (bK' : Fin _ → L)))
    (hM'_ge : Set.range (bK' : Fin _ → L) ⊆ M')
    (hD : latticeDiscriminant A K M' = latticeDiscriminant A K M) :
    M' = M

Uses 2

Statement usesDiscriminant of a lattice

Proof usesEqual discriminants force equal lattices

DefinitionImage of \(B\) in \(L\)#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(L\) a field, with algebra maps \(A \to B\), \(B \to L\) and \(A \to L\) forming a scalar tower. The image of \(B\) in \(L\) is the range of the algebra map \(B \to L\), regarded as an \(A\)-submodule of \(L\).

def imageOfB : Submodule A L :=
  Subalgebra.toSubmodule (IsScalarTower.toAlgHom A B L).range

Used by 6

Used byElements of \(B\) lie in the image of \(B\) · Discriminants of tuples from \(B\) lie in the extension discriminant · Extension discriminant · The extension discriminant is a lattice discriminant · Localization of the extension discriminant · Membership in the image of \(B\)

TheoremMembership in the image of \(B\)#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(L\) a field, with algebra maps \(A \to B\), \(B \to L\) and \(A \to L\) forming a scalar tower. An element \(x \in L\) lies in the image of \(B\) in \(L\) if and only if \(x\) is the image of some \(b \in B\) under the algebra map \(B \to L\).

theorem mem_imageOfB {x : L} :
    x ∈ imageOfB A L B ↔ ∃ b : B, algebraMap B L b = x

Uses 1 · Used by 2

Statement usesImage of \(B\) in \(L\)

Used byElements of \(B\) lie in the image of \(B\) · Localization of the extension discriminant

TheoremElements of \(B\) lie in the image of \(B\)#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(L\) a field, with algebra maps \(A \to B\), \(B \to L\) and \(A \to L\) forming a scalar tower. For every \(b \in B\), the image of \(b\) under the algebra map \(B \to L\) lies in the image of \(B\) in \(L\), regarded as an \(A\)-submodule of \(L\).

theorem algebraMap_mem_imageOfB (b : B) :
    algebraMap B L b ∈ imageOfB A L B

Uses 2

Statement usesImage of \(B\) in \(L\)

Proof usesMembership in the image of \(B\)

DefinitionExtension discriminant#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(K\) and \(L\) fields with \(L\) finite-dimensional over \(K\), with algebra maps forming scalar towers \(A \to K \to L\) and \(A \to B \to L\), and let \(n = [L : K]\). The extension discriminant is the \(A\)-submodule of \(K\) spanned by the discriminants \(\operatorname{disc}_{L/K}(b_1, \dots, b_n)\) of all \(n\)-tuples of elements of \(L\) lying in the image of \(B\) in \(L\).

At this level of generality it is only an \(A\)-submodule of \(K\), not an ideal of \(A\).

def extensionDiscriminant : Submodule A K :=
  latticeDiscriminant A K (imageOfB A L B)

Uses 2 · Used by 3

Statement usesImage of \(B\) in \(L\) · Discriminant of a lattice

Used byDiscriminants of tuples from \(B\) lie in the extension discriminant · The extension discriminant is a lattice discriminant · Localization of the extension discriminant

TheoremThe extension discriminant is a lattice discriminant#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(K\) and \(L\) fields with \(L\) finite-dimensional over \(K\), with algebra maps forming scalar towers \(A \to K \to L\) and \(A \to B \to L\). The extension discriminant of the tower equals the lattice discriminant over \(A\) and \(K\) of the image of \(B\) in \(L\), regarded as an \(A\)-submodule of \(L\).

theorem extensionDiscriminant_eq :
    extensionDiscriminant A K L B =
      latticeDiscriminant A K (imageOfB A L B)

Uses 3 · Used by 1

Statement usesExtension discriminant · Image of \(B\) in \(L\) · Discriminant of a lattice

Used byLocalization of the extension discriminant

TheoremDiscriminants of tuples from \(B\) lie in the extension discriminant#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(K\) and \(L\) fields with \(L\) finite-dimensional over \(K\), with algebra maps forming scalar towers \(A \to K \to L\) and \(A \to B \to L\), and let \(n = [L : K]\). If \(b_1, \dots, b_n \in L\) all lie in the image of \(B\) in \(L\), then their discriminant \(\operatorname{disc}_{L/K}(b_1, \dots, b_n)\) lies in the extension discriminant of the tower, an \(A\)-submodule of \(K\).

theorem discr_mem_extensionDiscriminant
    {b : Fin (Module.finrank K L) → L} (hb : ∀ i, b i ∈ imageOfB A L B) :
    Algebra.discr K b ∈ extensionDiscriminant A K L B

Uses 4 · Used by 1

Statement usesExtension discriminant · Image of \(B\) in \(L\)

Proof usesDiscriminant of a lattice · Discriminants of tuples from a submodule

Used byLocalization of the extension discriminant

TheoremLocalization of the extension discriminant#✓fully proved

Let \(A\) and \(B\) be commutative rings and \(K\) and \(L\) fields, with ring maps \(A \to K \to L\) and \(A \to B \to L\) whose composites \(A \to L\) agree, and with \(L\) finite-dimensional over \(K\) of degree \(n\). Write \(D_{B/A}\) for the \(A\)-submodule of \(K\) generated by the discriminants \(\operatorname{disc}_{L/K}(b_1, \dots, b_n)\) of all \(n\)-tuples of elements of the image of \(B\) in \(L\). Let \(S\) be a submonoid of \(A\), let \(S^{-1}A\) be a localization of \(A\) at \(S\), and let \(S^{-1}B\) be a localization of \(B\) at the image of \(S\) in \(B\). Suppose given ring maps \(S^{-1}A \to K\), \(S^{-1}A \to S^{-1}B\) and \(S^{-1}B \to L\) such that the composite \(A \to S^{-1}A \to K\) is the map \(A \to K\), the composite \(B \to S^{-1}B \to L\) is the map \(B \to L\), and the composites \(S^{-1}A \to K \to L\) and \(S^{-1}A \to S^{-1}B \to L\) agree. Then the \(S^{-1}A\)-submodule of \(K\) spanned by \(D_{B/A}\) equals \(D_{S^{-1}B/S^{-1}A}\), the \(S^{-1}A\)-submodule of \(K\) generated by the discriminants of \(n\)-tuples of elements of the image of \(S^{-1}B\) in \(L\).

No Dedekind, fraction-ring, integrally-closed, or separability hypotheses are used.

theorem extensionDiscriminant_localization :
    Submodule.span SA (extensionDiscriminant A K L B : Set K) =
      extensionDiscriminant SA K L SB

Uses 7

Statement usesExtension discriminant

Proof usesDiscriminants of tuples from \(B\) lie in the extension discriminant · The extension discriminant is a lattice discriminant · Image of \(B\) in \(L\) · Discriminant of a lattice · Discriminants of tuples from a submodule · Membership in the image of \(B\)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.