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)
43structure RSIndependentTriple (n : ℕ) where
44 axis1 : CoupledAxis n
45 axis2 : CoupledAxis n
46 axis3 : CoupledAxis n
47 indep12 : independent axis1 axis2
48 indep13 : independent axis1 axis3
49 indep23 : independent axis2 axis3
50
51/-- Pairwise independent disjoint sum of same-size axes. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
triple_card
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
tripleProductCard
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
axis1
in IndisputableMonolith.Algebra.F2Power
decl_use
-
axis2
in IndisputableMonolith.Algebra.F2Power
decl_use
-
axis3
in IndisputableMonolith.Algebra.F2Power
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
independent
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
CoupledAxis
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
independent
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use