No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
181theorem involutionOp_shiftOp (p : Nat.Primes) :
182 involutionOp ∘ₗ shiftOp p = shiftInvOp p ∘ₗ involutionOp := by
proof body
Term-mode proof.
183 ext v
184 simp only [LinearMap.coe_comp, Function.comp_apply,
185 shiftOp_single, involutionOp_single, shiftInvOp_single,
186 Finsupp.lsingle_apply]
187 congr 1
188 abel
189
190/-- Symmetric form of the previous: `U ∘ V_p^{-1} = V_p ∘ U`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
comp_apply
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Primes
in IndisputableMonolith.NumberTheory.EulerInstantiation
decl_use
-
involutionOp
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
involutionOp_single
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
shiftInvOp
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
shiftInvOp_single
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
shiftOp
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
shiftOp_single
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use