NYLL
Module

FixedFields.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.FixedFields
23 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: decomposition and inertia fields

This file contains the fixed-field layer of prime-decomposition theory. The Dedekind-domain file defines the decomposition and inertia groups attached to a prime ideal; here we view those groups as subgroups of a finite Galois group acting on the fraction field and use mathlib's Galois correspondence.

Imports1
Imported by5

Declarations

abbrev

fixedFieldOfSubgroup

L34 ↗
HilbertRamification.Dedekind.fixedFieldOfSubgroup
Documentation

The fixed field of a subgroup of a finite Galois group, in the IsGaloisGroup formulation used by the Dedekind ramification API.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
abbrev fixedFieldOfSubgroup (H : Subgroup G) : IntermediateField K L
theorem

mem_fixedFieldOfSubgroup_iff

L41 ↗
HilbertRamification.Dedekind.mem_fixedFieldOfSubgroup_iff
Documentation

Elementwise membership in the fixed field of a subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
Lean source · statement
theorem mem_fixedFieldOfSubgroup_iff
    {H : Subgroup G} {x : L} :
    x ∈ fixedFieldOfSubgroup (K := K) (L := L) G H ↔
      ∀ σ : H, (σ : G) • x = x
theorem

mem_fixedFieldOfSubgroup_iff_forall_mem

L49 ↗
HilbertRamification.Dedekind.mem_fixedFieldOfSubgroup_iff_forall_mem
Documentation

Membership in a subgroup fixed field, written with subgroup membership rather than subtype elements.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
Lean source · statement
theorem mem_fixedFieldOfSubgroup_iff_forall_mem
    {H : Subgroup G} {x : L} :
    x ∈ fixedFieldOfSubgroup (K := K) (L := L) G H ↔
      ∀ σ ∈ H, σ • x = x
theorem

fixedFieldOfSubgroup_fixingSubgroup_eq

L59 ↗
HilbertRamification.Dedekind.fixedFieldOfSubgroup_fixingSubgroup_eq
Documentation

The subgroup fixing the fixed field of a subgroup is the subgroup itself.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
theorem fixedFieldOfSubgroup_fixingSubgroup_eq
    (H : Subgroup G) [Finite G] [IsGaloisGroup G K L] :
    fixingSubgroup G
        ((fixedFieldOfSubgroup (K := K) (L := L) G H : IntermediateField K L) :
          Set L) =
      H
theorem

fixedFieldOfSubgroup_eq_top_iff_subgroup_eq_bot

L72 ↗
HilbertRamification.Dedekind.fixedFieldOfSubgroup_eq_top_iff_subgroup_eq_bot
Documentation

A subgroup has full fixed field exactly when it is trivial.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem fixedFieldOfSubgroup_eq_top_iff_subgroup_eq_bot
    {H : Subgroup G} [Finite G] [IsGaloisGroup G K L] :
    fixedFieldOfSubgroup (K := K) (L := L) G H = ⊤ ↔ H = ⊥
theorem

fixedFieldOfSubgroup_eq_bot_iff_subgroup_eq_top

L92 ↗
HilbertRamification.Dedekind.fixedFieldOfSubgroup_eq_bot_iff_subgroup_eq_top
Documentation

A subgroup has base fixed field exactly when it is all of the Galois group.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem fixedFieldOfSubgroup_eq_bot_iff_subgroup_eq_top
    {H : Subgroup G} [Finite G] [IsGaloisGroup G K L] :
    fixedFieldOfSubgroup (K := K) (L := L) G H = ⊥ ↔ H = ⊤
abbrev

decompositionField

L116 ↗
HilbertRamification.Dedekind.decompositionField
Documentation

The decomposition and inertia definition: the decomposition field Z_P, as the fixed field of the decomposition group.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
abbrev decompositionField
    (P : Ideal B) [MulSemiringAction G B] : IntermediateField K L
theorem

mem_decompositionField_iff

L124 ↗
HilbertRamification.Dedekind.mem_decompositionField_iff
Documentation

Elementwise membership in the decomposition field.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem mem_decompositionField_iff
    {P : Ideal B} [MulSemiringAction G B] {x : L} :
    x ∈ decompositionField (K := K) (L := L) G P ↔
      ∀ σ ∈ decompositionGroup P G, σ • x = x
theorem

dedekindDecomposition_decompositionField_fixingSubgroup_eq

L134 ↗
HilbertRamification.Dedekind.dedekindDecomposition_decompositionField_fixingSubgroup_eq
Documentation

Decomposition and inertia groups satisfy: the subgroup fixing the decomposition field is the decomposition group.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindDecomposition_decompositionField_fixingSubgroup_eq
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    fixingSubgroup G
        ((decompositionField (K := K) (L := L) G P : IntermediateField K L) :
          Set L) =
      decompositionGroup P G
theorem

dedekindDecomposition_decompositionField_eq_top_iff_decompositionGroup_eq_bot

L147 ↗
HilbertRamification.Dedekind.dedekindDecomposition_decompositionField_eq_top_iff_decompositionGroup_eq_bot
Documentation

Decomposition and inertia groups satisfy: G_P = 1 if and only if Z_P = L.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindDecomposition_decompositionField_eq_top_iff_decompositionGroup_eq_bot
    {P : Ideal B} [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    decompositionField (K := K) (L := L) G P = ⊤ ↔
      decompositionGroup P G = ⊥
theorem

dedekindDecomposition_decompositionField_eq_bot_iff_decompositionGroup_eq_top

L158 ↗
HilbertRamification.Dedekind.dedekindDecomposition_decompositionField_eq_bot_iff_decompositionGroup_eq_top
Documentation

Decomposition and inertia groups satisfy: G_P = G if and only if Z_P = K.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindDecomposition_decompositionField_eq_bot_iff_decompositionGroup_eq_top
    {P : Ideal B} [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    decompositionField (K := K) (L := L) G P = ⊥ ↔
      decompositionGroup P G = ⊤
theorem

dedekindDecomposition_decompositionField_eq_top_iff_primesOver_ncard_eq_card

L170 ↗
HilbertRamification.Dedekind.dedekindDecomposition_decompositionField_eq_top_iff_primesOver_ncard_eq_card
Documentation

Decomposition and inertia groups satisfy: the fixed-field form of total splitting, Z_P = L iff the number of primes above p is #G.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindDecomposition_decompositionField_eq_top_iff_primesOver_ncard_eq_card
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] [IsGaloisGroup G A B] :
    decompositionField (K := K) (L := L) G P = ⊤ ↔
      (p.primesOver B).ncard = Nat.card G
theorem

dedekindDecomposition_decompositionField_eq_bot_iff_primesOver_ncard_eq_one

L184 ↗
HilbertRamification.Dedekind.dedekindDecomposition_decompositionField_eq_bot_iff_primesOver_ncard_eq_one
Documentation

Decomposition and inertia groups satisfy: the fixed-field form of nonsplitting, Z_P = K iff P is the only prime above p.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindDecomposition_decompositionField_eq_bot_iff_primesOver_ncard_eq_one
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] [IsGaloisGroup G A B] :
    decompositionField (K := K) (L := L) G P = ⊥ ↔
      (p.primesOver B).ncard = 1
theorem

dedekindTower_decompositionField_finrank_eq_decomposition_card

L199 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionField_finrank_eq_decomposition_card
Documentation

The prime-decomposition tower identity: [L : Z_P] = #G_P.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindTower_decompositionField_finrank_eq_decomposition_card
    (P : Ideal B) [MulSemiringAction G B] [IsGaloisGroup G K L] :
    Module.finrank (decompositionField (K := K) (L := L) G P) L =
      Nat.card (decompositionGroup P G)
instance

decompositionGroup_isGaloisGroup

L209 ↗
HilbertRamification.Dedekind.decompositionGroup_isGaloisGroup
Documentation

The prime-decomposition tower identity: the decomposition group is the Galois group of L/Z_P.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
instance decompositionGroup_isGaloisGroup
    (P : Ideal B) [MulSemiringAction G B] [IsGaloisGroup G K L] :
    IsGaloisGroup (decompositionGroup P G)
      (decompositionField (K := K) (L := L) G P) L
abbrev

inertiaField

L218 ↗
HilbertRamification.Dedekind.inertiaField
Documentation

The inertia-field definition: the inertia field T_P, as the fixed field of the inertia group.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
abbrev inertiaField
    (P : Ideal B) [MulSemiringAction G B] : IntermediateField K L
theorem

mem_inertiaField_iff

L226 ↗
HilbertRamification.Dedekind.mem_inertiaField_iff
Documentation

Elementwise membership in the inertia field.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem mem_inertiaField_iff
    {P : Ideal B} [MulSemiringAction G B] {x : L} :
    x ∈ inertiaField (K := K) (L := L) G P ↔
      ∀ σ ∈ inertiaGroup P G, σ • x = x
theorem

decompositionField_le_inertiaField

L236 ↗
HilbertRamification.Dedekind.decompositionField_le_inertiaField
Documentation

Prime-decomposition statement: the decomposition field is contained in the inertia field.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem decompositionField_le_inertiaField
    (P : Ideal B) [MulSemiringAction G B] :
    decompositionField (K := K) (L := L) G P ≤
      inertiaField (K := K) (L := L) G P
theorem

dedekindRamification_inertiaField_fixingSubgroup_eq

L252 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_fixingSubgroup_eq
Documentation

Prime-decomposition statement: the subgroup fixing the inertia field is the inertia group.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindRamification_inertiaField_fixingSubgroup_eq
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    fixingSubgroup G
        ((inertiaField (K := K) (L := L) G P : IntermediateField K L) :
          Set L) =
      inertiaGroup P G
theorem

dedekindRamification_inertiaField_eq_top_iff_inertiaGroup_eq_bot

L265 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_eq_top_iff_inertiaGroup_eq_bot
Documentation

A fixed-field special case: I_P = 1 if and only if T_P = L.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindRamification_inertiaField_eq_top_iff_inertiaGroup_eq_bot
    {P : Ideal B} [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    inertiaField (K := K) (L := L) G P = ⊤ ↔
      inertiaGroup P G = ⊥
theorem

dedekindRamification_inertiaField_eq_bot_iff_inertiaGroup_eq_top

L276 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_eq_bot_iff_inertiaGroup_eq_top
Documentation

Fixed-field source for the opposite extreme of the inertia field: I_P = G if and only if T_P = K.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem dedekindRamification_inertiaField_eq_bot_iff_inertiaGroup_eq_top
    {P : Ideal B} [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    inertiaField (K := K) (L := L) G P = ⊥ ↔
      inertiaGroup P G = ⊤
theorem

dedekindRamification_inertiaField_finrank_eq_inertia_card

L289 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_finrank_eq_inertia_card
Documentation

A prime-decomposition consequence: [L : T_P] = #I_P.

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindRamification_inertiaField_finrank_eq_inertia_card
    (P : Ideal B) [MulSemiringAction G B] [IsGaloisGroup G K L] :
    Module.finrank (inertiaField (K := K) (L := L) G P) L =
      Nat.card (inertiaGroup P G)
instance

inertiaGroup_isGaloisGroup

L299 ↗
HilbertRamification.Dedekind.inertiaGroup_isGaloisGroup
Documentation

A prime-decomposition consequence: the inertia group is the Galois group of L/T_P.

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
instance inertiaGroup_isGaloisGroup
    (P : Ideal B) [MulSemiringAction G B] [IsGaloisGroup G K L] :
    IsGaloisGroup (inertiaGroup P G)
      (inertiaField (K := K) (L := L) G P) L

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.