structure definition def or abbrev

`CkmMixingAngles`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  26structure CkmMixingAngles where
  27  vus : ℝ
  28  vcb : ℝ
  29  vub : ℝ
  30
  31namespace LeptonMassRatios
  32
  33/-- Canonical list view: `[μ/e, τ/e, τ/μ]`. -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

mixingFromCycles in IndisputableMonolith.RecogSpec.BridgeDerivation decl_use
DimlessPack in IndisputableMonolith.RecogSpec.Core decl_use
UniversalDimless in IndisputableMonolith.RecogSpec.Core decl_use
ext in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
Forall in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
forall_iff_list in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
mk_toList in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
mk_toList in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
toList in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
toList_injective in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
toList_length in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use

depends on (1)

Lean names referenced from this declaration's body.

LeptonMassRatios in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use