Metric

used by (40)

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

• coeff_bound_of_uniformBounds in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
• exists_integral_ne_zero in IndisputableMonolith.Cost.AczelProof decl_use
• exists_integral_ne_zero in IndisputableMonolith.Cost.AczelTheorem decl_use
• SelfSustaining in IndisputableMonolith.Energy.VacuumPump decl_use
• simplicial_foundation_status in IndisputableMonolith.Foundation.SimplicialFoundationSummary decl_use
• christoffel_symmetric in IndisputableMonolith.Gravity.Connection decl_use
• Idx in IndisputableMonolith.Gravity.Connection decl_use
• delta_H0_positive in IndisputableMonolith.Gravity.HubbleTension decl_use
• H_HomogenizationLimit in IndisputableMonolith.Meta.Homogenization decl_use
• constructive_at_zero in IndisputableMonolith.Modal.ModalGeometry decl_use
• bounded_subseq_tendsto in IndisputableMonolith.NavierStokes.FourierExtraction decl_use
• D_converges in IndisputableMonolith.NavierStokes.FourierExtraction decl_use
• lipschitz_dense_extension in IndisputableMonolith.NavierStokes.GalerkinEquicontinuity decl_use
• coerciveL2Bound_of_tailFluxVanish in IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity decl_use
• ancientDecay_implies_tailFlux_vanish in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
• rescaleLength_tendsto_zero in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
• rigid_rotation_energy_lower_bound in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
• rigid_rotation_infinite_energy in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
• rigid_rotation_infinite_energy_proved in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
• holomorphic_circle_integral_zero in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• holomorphic_nonvanishing_zero_charge in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• logDeriv_circle_integral_zero in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• mkRegularFactorPhase in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• regularFactor_continuousPhase_exists in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• regularFactor_phase_lipschitz in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• winding_integral_simple_pole in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• zpow_charge_eq_winding_integral in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
• ComplexCarrierCert in IndisputableMonolith.NumberTheory.EulerCarrierComplex decl_use
• mkComplexCarrierCert in IndisputableMonolith.NumberTheory.EulerCarrierComplex decl_use
• local_meromorphic_factorization in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use

… and 10 more