theorem
proved
term proof
solar_correction_geometric
show as:
view Lean formalization →
formal statement (Lean)
223theorem solar_correction_geometric :
224 solar_radiative_correction = PMNSCorrections.solar_correction := by
proof body
Term-mode proof.
225 simpa using (PMNSCorrections.solar_matches).symm
226
227/-- **CERTIFICATE: Mixing Matrix Geometry**
228 Packages the proofs for CKM and PMNS mixing parameters. -/