NYLL
Module

AddCommGroup.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup
20 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — add comm group

The principal declarations in this module are:

  • instAddCommGroupModNCompletedGroupAlgebraStage

Each finite mod-\(n\) group-algebra stage carries its standard additive commutative group.

  • instAddCommGroupModNCompletedGroupAlgebraFamily

The dependent family of finite mod-\(n\) group-algebra stages carries the pointwise additive commutative group structure.

  • coe_zero_modNCompletedGroupAlgebra

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.

  • coe_add_modNCompletedGroupAlgebra

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.

Imports1
Imported by2

Declarations

instance

instZeroModNCompletedGroupAlgebra

L44 ↗
FoxDifferential.instZeroModNCompletedGroupAlgebra
Documentation

The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instZeroModNCompletedGroupAlgebra : Zero (ModNCompletedGroupAlgebra n G) where
  zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStage n G U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransition n G hUV
      (0 : ModNCompletedGroupAlgebraStage n G V) = 0
    exact map_zero (modNCompletedGroupAlgebraTransition n G hUV)⟩
instance

instAddModNCompletedGroupAlgebra

L55 ↗
FoxDifferential.instAddModNCompletedGroupAlgebra
Documentation

Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddModNCompletedGroupAlgebra : Add (ModNCompletedGroupAlgebra n G) where
  add x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
        (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
    intro U V hUV
    calc
      modNCompletedGroupAlgebraTransition n G hUV
          ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
            (show ModNCompletedGroupAlgebraStage n G V from y.1 V))
        =
          modNCompletedGroupAlgebraTransition n G hUV
              (show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
            modNCompletedGroupAlgebraTransition n G hUV
              (show ModNCompletedGroupAlgebraStage n G V from y.1 V) := by
            rw [map_add]
      _ =
          (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
            (show ModNCompletedGroupAlgebraStage n G U from y.1 U) := by
            exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
instance

instAddZeroClassModNCompletedGroupAlgebra

L79 ↗
FoxDifferential.instAddZeroClassModNCompletedGroupAlgebra
Documentation

Coordinatewise zero and addition on the mod-\(n\) completed group algebra satisfy the left and right zero laws.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddZeroClassModNCompletedGroupAlgebra :
    AddZeroClass (ModNCompletedGroupAlgebra n G) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext U
    change (0 : ModNCompletedGroupAlgebraStage n G U) +
      (show ModNCompletedGroupAlgebraStage n G U from x.1 U) =
        (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
    exact zero_add (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
  add_zero x := by
    apply Subtype.ext
    funext U
    change (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
      (0 : ModNCompletedGroupAlgebraStage n G U) =
        (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
    exact add_zero (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
instance

instNegModNCompletedGroupAlgebra

L102 ↗
FoxDifferential.instNegModNCompletedGroupAlgebra
Documentation

Negation on the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra negations.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instNegModNCompletedGroupAlgebra : Neg (ModNCompletedGroupAlgebra n G) where
  neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransition n G hUV
        (-(show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
      -(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 U V hUV)⟩
instance

instSubModNCompletedGroupAlgebra

L115 ↗
FoxDifferential.instSubModNCompletedGroupAlgebra
Documentation

Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSubModNCompletedGroupAlgebra : Sub (ModNCompletedGroupAlgebra n G) where
  sub x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
        (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransition n G hUV
        ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) -
          (show ModNCompletedGroupAlgebraStage n G V from y.1 V)) =
      (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
        (show ModNCompletedGroupAlgebraStage n G U from y.1 U)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
instance

instSMulNatModNCompletedGroupAlgebra

L132 ↗
FoxDifferential.instSMulNatModNCompletedGroupAlgebra
Documentation

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulNatModNCompletedGroupAlgebra : SMul ℕ (ModNCompletedGroupAlgebra n G) where
  smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransition n G hUV
        (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩
instance

instSMulIntModNCompletedGroupAlgebra

L145 ↗
FoxDifferential.instSMulIntModNCompletedGroupAlgebra
Documentation

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulIntModNCompletedGroupAlgebra : SMul ℤ (ModNCompletedGroupAlgebra n G) where
  smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransition n G hUV
        (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩
def

instAddCommGroupModNCompletedGroupAlgebraStage

L156 ↗
FoxDifferential.instAddCommGroupModNCompletedGroupAlgebraStage
Documentation

Each finite mod-\(n\) group-algebra stage carries its standard additive commutative group.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def instAddCommGroupModNCompletedGroupAlgebraStage (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    AddCommGroup ((modNCompletedGroupAlgebraSystem n G).X U)
def

instAddCommGroupModNCompletedGroupAlgebraFamily

L168 ↗
FoxDifferential.instAddCommGroupModNCompletedGroupAlgebraFamily
Documentation

The dependent family of finite mod-\(n\) group-algebra stages carries the pointwise additive commutative group structure.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
Lean source · statement
def instAddCommGroupModNCompletedGroupAlgebraFamily :
    AddCommGroup ((i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
        (modNCompletedGroupAlgebraSystem n G).X i)
theorem

coe_zero_modNCompletedGroupAlgebra

L180 ↗
FoxDifferential.coe_zero_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_zero_modNCompletedGroupAlgebra :
    ((0 : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) = 0
theorem

coe_add_modNCompletedGroupAlgebra

L193 ↗
FoxDifferential.coe_add_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_add_modNCompletedGroupAlgebra
    (x y : ModNCompletedGroupAlgebra n G) :
    ((x + y : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) =
      x + y
theorem

coe_neg_modNCompletedGroupAlgebra

L208 ↗
FoxDifferential.coe_neg_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_neg_modNCompletedGroupAlgebra
    (x : ModNCompletedGroupAlgebra n G) :
    ((-x : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) =
      -x
theorem

coe_sub_modNCompletedGroupAlgebra

L223 ↗
FoxDifferential.coe_sub_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_sub_modNCompletedGroupAlgebra
    (x y : ModNCompletedGroupAlgebra n G) :
    ((x - y : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) =
      x - y
theorem

coe_nsmul_modNCompletedGroupAlgebra

L238 ↗
FoxDifferential.coe_nsmul_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves natural-number scalar multiplication.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_nsmul_modNCompletedGroupAlgebra
    (m : ℕ) (x : ModNCompletedGroupAlgebra n G) :
    ((m • x : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) =
      m • x
theorem

coe_zsmul_modNCompletedGroupAlgebra

L253 ↗
FoxDifferential.coe_zsmul_modNCompletedGroupAlgebra
Documentation

The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves integer scalar multiplication.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_zsmul_modNCompletedGroupAlgebra
    (m : ℤ) (x : ModNCompletedGroupAlgebra n G) :
    ((m • x : ModNCompletedGroupAlgebra n G) :
      (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
          (modNCompletedGroupAlgebraSystem n G).X i) =
      m • x
instance

instAddCommGroupModNCompletedGroupAlgebra

L266 ↗
FoxDifferential.instAddCommGroupModNCompletedGroupAlgebra
Documentation

The mod-\(n\) completion inherits an additive commutative group structure from its injective inclusion into the family of finite stages.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
Lean source · statement
instance instAddCommGroupModNCompletedGroupAlgebra :
    AddCommGroup (ModNCompletedGroupAlgebra n G)
theorem

modNCompletedGroupAlgebraProjection_zero

L283 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_zero
Documentation

The finite-stage projection sends \(0\) to \(0\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_zero (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    modNCompletedGroupAlgebraProjection n G U (0 : ModNCompletedGroupAlgebra n G) = 0
theorem

modNCompletedGroupAlgebraProjection_add

L292 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_add
Documentation

The mod-\(n\) finite-stage projection preserves addition.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_add (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x y : ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraProjection n G U (x + y) =
      modNCompletedGroupAlgebraProjection n G U x +
        modNCompletedGroupAlgebraProjection n G U y
theorem

modNCompletedGroupAlgebraProjection_neg

L306 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_neg
Documentation

The mod-\(n\) finite-stage projection preserves negation.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_neg (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x : ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraProjection n G U (-x) =
      -modNCompletedGroupAlgebraProjection n G U x
theorem

modNCompletedGroupAlgebraProjection_sub

L318 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_sub
Documentation

The mod-\(n\) finite-stage projection preserves subtraction.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_sub (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x y : ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraProjection n G U (x - y) =
      modNCompletedGroupAlgebraProjection n G U x -
        modNCompletedGroupAlgebraProjection n G U y

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