Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/Projection

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection

8 Theorems

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraProjectionInClass_one The finite-stage projection sends \(1\) to \(1\). - primePowerCompletedGroupAlgebraProjectionInClass_mul The finite-stage projection preserves multiplication. - primePowerCompletedGroupAlgebraProjectionInClass_zero The finite-stage projection sends \(0\) to \(0\). - primePowerCompletedGroupAlgebraProjectionInClass_add The prime-power finite-stage projection preserves addition.
import
Imported by

Declarations

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_one 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_one
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
        (1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 1

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_mul 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_mul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x * y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x *
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y

The finite-stage projection preserves multiplication.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_zero 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_zero
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
      (0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 0

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_add 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_add
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x +
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y

The prime-power finite-stage projection preserves addition.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_neg 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_neg
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
      -primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x

The prime-power finite-stage projection preserves negation.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_sub 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_sub
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x -
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y

The prime-power finite-stage projection preserves subtraction.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_nsmul 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_nsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
      m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x

The finite-stage projection is compatible with natural-number scalar multiplication.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_zsmul 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_zsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
      m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x

The finite-stage projection is compatible with integer scalar multiplication.

Show Lean proof