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)
22structure PMNSUnitarity (U : Matrix (Fin 3) (Fin 3) ℂ) : Prop where
23 unitary : Matrix.IsUnitary U
24 matches_weights : ∀ i j, ‖U i j‖ ^ 2 =
25 pmns_weight (IndisputableMonolith.RSBridge.rung (match i with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3) -
26 IndisputableMonolith.RSBridge.rung (match j with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3)) / 3
27
28end IndisputableMonolith.Physics.PMNS
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
pmns_weight
in IndisputableMonolith.Physics.MixingDerivation
decl_use
-
pmns_weight
in IndisputableMonolith.Physics.PMNS.Types
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use
-
RSBridge
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
IsUnitary
in IndisputableMonolith.Support.MatrixProperties
decl_use