NYLL
Module

Quotient.lean

Nyll.ValuedFieldTheory.Ramification.Herbrand.Quotient
25 declarations indexed from sourceView source ↗

Module documentation

Pure group theory for Herbrand towers

This file contains the completion-free finite-group bookkeeping used in the Herbrand quotient theorem and the quotient and tower filtration theorems. It packages the filtrations induced on a subgroup and on its quotient image, proves the exact cardinality factorization at every level, and records compatibility of Herbrand functions with transport along group equivalences.

The valued-field inputs of the quotient-depth and upper-numbering identities do not occur here. Valued-field endpoints combine these structural lemmas with ramification-number averaging; the inverse-function and upper-numbering statements are proved directly in the Hilbert-ramification Herbrand theorem module.

Imports3
Imported by2

Declarations

def

subgroupFiltration

L39 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subgroupFiltration
Documentation

The filtration induced on a subgroup by intersection with every ambient lower group.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · full declaration
def subgroupFiltration (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) :
    AntitoneNormalSubgroupFiltration H where
  lower n := (F.lower n).comap H.subtype
  lower_normal n := (F.lower_normal n).comap H.subtype
  antitone := by
    intro m n hmn
    exact Subgroup.comap_mono (F.antitone hmn)
theorem

subgroupFiltration_lower

L48 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subgroupFiltration_lower
Documentation

States the theorem subgroupFiltration_lower.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · statement
theorem subgroupFiltration_lower
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) (n : ℕ) :
    (subgroupFiltration F H).lower n = (F.lower n).comap H.subtype
theorem

mem_subgroupFiltration_lower_iff

L54 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.mem_subgroupFiltration_lower_iff
Documentation

States the theorem mem_subgroupFiltration_lower_iff.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · statement
theorem mem_subgroupFiltration_lower_iff
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G)
    (n : ℕ) (h : H) :
    h ∈ (subgroupFiltration F H).lower n ↔ (h : G) ∈ F.lower n
def

quotientImageFiltration

L63 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageFiltration
Documentation

The pointwise image filtration on a quotient by a normal subgroup. This is not asserted to be the actual lower filtration of a valued quotient; that identification is precisely the content supplied by Herbrand's theorem.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · full declaration
def quotientImageFiltration (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] :
    AntitoneNormalSubgroupFiltration (G ⧸ H) where
  lower n := (F.lower n).map (QuotientGroup.mk' H)
  lower_normal n := (F.lower_normal n).map
    (QuotientGroup.mk' H) (QuotientGroup.mk'_surjective H)
  antitone := by
    intro m n hmn
    exact Subgroup.map_mono (F.antitone hmn)
theorem

quotientImageFiltration_lower

L74 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageFiltration_lower
Documentation

States the theorem quotientImageFiltration_lower.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · statement
theorem quotientImageFiltration_lower
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (n : ℕ) :
    (quotientImageFiltration F H).lower n =
      (F.lower n).map (QuotientGroup.mk' H)
def

lowerToQuotientImageHom

L83 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lowerToQuotientImageHom
Documentation

At each level, the subgroup filtration is the kernel of the quotient map restricted to the corresponding ambient lower group.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · full declaration
def lowerToQuotientImageHom (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] (n : ℕ) :
    F.lower n →* (quotientImageFiltration F H).lower n where
  toFun sigma :=
    ⟨QuotientGroup.mk' H (sigma : G), ⟨sigma, sigma.property, rfl⟩⟩
  map_one' := by
    apply Subtype.ext
    simp
  map_mul' sigma tau := by
    apply Subtype.ext
    change QuotientGroup.mk' H (((sigma * tau : F.lower n) : G)) =
      QuotientGroup.mk' H (sigma : G) * QuotientGroup.mk' H (tau : G)
    rw [show (((sigma * tau : F.lower n) : G)) =
      (sigma : G) * (tau : G) by rfl, map_mul]
theorem

lowerToQuotientImageHom_surjective

L99 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lowerToQuotientImageHom_surjective
Documentation

States the theorem lowerToQuotientImageHom_surjective.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · statement
theorem lowerToQuotientImageHom_surjective
    (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] (n : ℕ) :
    Function.Surjective (lowerToQuotientImageHom F H n)
def

lowerToQuotientImageKerEquiv

L111 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lowerToQuotientImageKerEquiv
Documentation

The kernel of the restricted quotient map is canonically the intersection filtration on H.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · full declaration
def lowerToQuotientImageKerEquiv (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] (n : ℕ) :
    (lowerToQuotientImageHom F H n).ker ≃
      (subgroupFiltration F H).lower n where
  toFun sigma := by
    let sigmaLower : F.lower n := sigma
    have hmk : QuotientGroup.mk' H ((sigma : F.lower n) : G) = 1 := by
      exact congrArg Subtype.val sigma.property
    have hsigmaH : ((sigma : F.lower n) : G) ∈ H :=
      (QuotientGroup.eq_one_iff (N := H)
        (x := ((sigma : F.lower n) : G))).1 hmk
    exact ⟨⟨((sigma : F.lower n) : G), hsigmaH⟩, sigmaLower.property⟩
  invFun h := by
    refine ⟨⟨((h : H) : G), h.property⟩, ?_⟩
    apply Subtype.ext
    exact (QuotientGroup.eq_one_iff (N := H) (x := ((h : H) : G))).2 h.val.property
  left_inv sigma := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
  right_inv h := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
theorem

card_subgroupFiltration_mul_card_quotientImageFiltration

L138 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_subgroupFiltration_mul_card_quotientImageFiltration
Documentation

Exact level-cardinality factorization |F_n| = |F_n ∩ H| * |image(F_n)|.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
Lean source · statement
theorem card_subgroupFiltration_mul_card_quotientImageFiltration
    [Finite G] (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] (n : ℕ) :
    Nat.card ((subgroupFiltration F H).lower n) *
        Nat.card ((quotientImageFiltration F H).lower n) =
      Nat.card (F.lower n)
def

transportEquiv

L159 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.transportEquiv
Documentation

Transport a lower ramification filtration across a group equivalence.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · full declaration
def transportEquiv (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') :
    AntitoneNormalSubgroupFiltration G' where
  lower n := (F.lower n).comap e.symm.toMonoidHom
  lower_normal n := (F.lower_normal n).comap e.symm.toMonoidHom
  antitone := by
    intro m n hmn
    exact Subgroup.comap_mono (F.antitone hmn)
theorem

transportEquiv_lower

L168 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.transportEquiv_lower
Documentation

States the theorem transportEquiv_lower.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem transportEquiv_lower
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (n : ℕ) :
    (transportEquiv F e).lower n =
      (F.lower n).comap e.symm.toMonoidHom
theorem

mem_transportEquiv_lower_iff

L175 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.mem_transportEquiv_lower_iff
Documentation

States the theorem mem_transportEquiv_lower_iff.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem mem_transportEquiv_lower_iff
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G')
    (n : ℕ) (sigma : G') :
    sigma ∈ (transportEquiv F e).lower n ↔ e.symm sigma ∈ F.lower n
def

lowerEquivTransportEquiv

L182 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lowerEquivTransportEquiv
Documentation

Every integral level is carried to the corresponding transported level.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · full declaration
def lowerEquivTransportEquiv
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (n : ℕ) :
    F.lower n ≃ (transportEquiv F e).lower n where
  toFun sigma := ⟨e (sigma : G), by simp⟩
  invFun tau := ⟨e.symm (tau : G'), tau.property⟩
  left_inv sigma := by
    apply Subtype.ext
    simp
  right_inv tau := by
    apply Subtype.ext
    simp
theorem

card_lower_transportEquiv

L195 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_lower_transportEquiv
Documentation

States the theorem card_lower_transportEquiv.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem card_lower_transportEquiv
    [Finite G] [Finite G']
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (n : ℕ) :
    Nat.card ((transportEquiv F e).lower n) = Nat.card (F.lower n)
theorem

herbrandFunction_transportEquiv

L207 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_transportEquiv
Documentation

The Herbrand function is invariant under transport across a group equivalence.

Source context 7 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_eq_of_card_lower_eq
) in
Lean source · statement
theorem herbrandFunction_transportEquiv
    [Finite G] [Finite G']
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (s : ℝ) :
    (herbrandFunction (transportEquiv F e)) s = (herbrandFunction F) s
theorem

inverseHerbrandFunction_transportEquiv

L223 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction_transportEquiv
Documentation

The inverse Herbrand function is invariant under transport across a group equivalence.

Source context 7 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction_inverseHerbrandFunction
  herbrandFunction_strictMono
  herbrandFunction_transportEquiv
  inverseHerbrandFunction
) in
Lean source · statement
theorem inverseHerbrandFunction_transportEquiv
    [Finite G] [Finite G']
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (t : ℝ) :
    (inverseHerbrandFunction (transportEquiv F e)) t = (inverseHerbrandFunction F) t
def

quotientImageTransport

L234 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageTransport
Documentation

The quotient-image filtration, transported to any isomorphic model of the quotient group.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
def quotientImageTransport
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (e : (G ⧸ H) ≃* G') : AntitoneNormalSubgroupFiltration G'
theorem

quotientImageTransport_lower

L240 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageTransport_lower
Documentation

States the theorem quotientImageTransport_lower.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem quotientImageTransport_lower
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (e : (G ⧸ H) ≃* G') (n : ℕ) :
    (quotientImageTransport F H e).lower n =
      ((F.lower n).map (QuotientGroup.mk' H)).comap e.symm.toMonoidHom
theorem

subgroup_map_equiv_eq_iff_eq_comap

L249 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subgroup_map_equiv_eq_iff_eq_comap
Documentation

Mapping a subgroup across a group equivalence is inverse to pulling it back. This orientation is the one used by the fixed-field quotient map.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem subgroup_map_equiv_eq_iff_eq_comap
    (e : G ≃* G') (A : Subgroup G) (B : Subgroup G') :
    A.map e.toMonoidHom = B ↔
      A = B.comap e.toMonoidHom
theorem

transportEquiv_lower_eq_map

L264 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.transportEquiv_lower_eq_map
Documentation

States the theorem transportEquiv_lower_eq_map.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem transportEquiv_lower_eq_map
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G') (n : ℕ) :
    (transportEquiv F e).lower n = (F.lower n).map e.toMonoidHom
theorem

transportEquiv_lower_eq_iff

L276 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.transportEquiv_lower_eq_iff
Documentation

States the theorem transportEquiv_lower_eq_iff.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem transportEquiv_lower_eq_iff
    (F : AntitoneNormalSubgroupFiltration G) (e : G ≃* G')
    (n : ℕ) (B : Subgroup G') :
    (transportEquiv F e).lower n = B ↔
      F.lower n = B.comap e.toMonoidHom
theorem

quotientImageTransport_lower_eq_iff

L286 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageTransport_lower_eq_iff
Documentation

Equality with a transported quotient-image level is exactly the usual map/comap formulation of a lower-quotient theorem.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem quotientImageTransport_lower_eq_iff
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (e : (G ⧸ H) ≃* G') (n : ℕ) (B : Subgroup G') :
    (quotientImageTransport F H e).lower n = B ↔
      (F.lower n).map (QuotientGroup.mk' H) =
        B.comap e.toMonoidHom
theorem

card_subgroupFiltration_mul_card_quotientImageTransport

L297 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_subgroupFiltration_mul_card_quotientImageTransport
Documentation

Exact level-cardinality factorization after replacing the abstract quotient by any isomorphic group model.

Source context 6 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
Lean source · statement
theorem card_subgroupFiltration_mul_card_quotientImageTransport
    [Finite G] [Finite G'] (F : AntitoneNormalSubgroupFiltration G)
    (H : Subgroup G) [H.Normal] (e : (G ⧸ H) ≃* G') (n : ℕ) :
    Nat.card ((subgroupFiltration F H).lower n) *
        Nat.card ((quotientImageTransport F H e).lower n) =
      Nat.card (F.lower n)
theorem

quotientImageTransport_herbrandFunction

L312 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageTransport_herbrandFunction
Documentation

States the theorem quotientImageTransport_herbrandFunction.

Source context 7 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
) in
Lean source · statement
theorem quotientImageTransport_herbrandFunction
    [Finite G] [Finite G']
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (e : (G ⧸ H) ≃* G') (s : ℝ) :
    (herbrandFunction (quotientImageTransport F H e)) s =
      (herbrandFunction (quotientImageFiltration F H)) s
theorem

quotientImageTransport_inverseHerbrandFunction

L325 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientImageTransport_inverseHerbrandFunction
Documentation

States the theorem quotientImageTransport_inverseHerbrandFunction.

Source context 7 commands

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

noncomputable section
universe u v
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G]
variable {G' : Type v} [Group G']
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  inverseHerbrandFunction
) in
Lean source · statement
theorem quotientImageTransport_inverseHerbrandFunction
    [Finite G] [Finite G']
    (F : AntitoneNormalSubgroupFiltration G) (H : Subgroup G) [H.Normal]
    (e : (G ⧸ H) ≃* G') (t : ℝ) :
    (inverseHerbrandFunction (quotientImageTransport F H e)) t =
      (inverseHerbrandFunction (quotientImageFiltration F H)) t

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